Skip to:Content
Cover image for Real-time systems : scheduling, analysis, and verification
Real-time systems : scheduling, analysis, and verification
Personal Author:
Publication Information:
Hoboken, NJ : Wiley Interscience, 2002


Item Barcode
Call Number
Material Type
Item Category 1
30000010018783 QA76.54 C33 2002 Open Access Book Book

On Order



The first book to provide a comprehensive overview of the subject rather than a collection of papers. The author is a recognized authority in the field as well as an outstanding teacher lauded for his ability to convey these concepts clearly to many different audiences. A handy reference for practitioners in the field.

Author Notes

ALBERT M. K. CHENG, PhD, received his doctorate in computer science from the University of Texas at Austin, where he held a GTE Foundation Doctoral Fellowship. He is currently an associate professor in the department of computer science at the University of Houston, where he is the founding director of the Real-Time Systems Laboratory. He is the author and coauthor of over sixty refereed publications, and has received numerous awards, including the NSF Career award. He has served as a technical consultant for several organizations, including IBM, and has served on the program committees of many conferences.

Table of Contents

List Of Figures
1 Introduction
1.1 What Is Time?
1.2 Simulation
1.3 Testing
1.4 Verification
1.5 Run-Time Monitoring
1.6 Useful Resources
2 Analysis and Verification of Non-Real-Time Systems
2.1 Symbolic Logic
2.2 Automata and Languages
2.3 Historical Perspective and Related Work
2.4 Summary
3 Real-Time Scheduling and Schedulability Analysis
3.1 Determining Computation Time
3.2 Uniprocessor Scheduling
3.3 Multiprocessor Scheduling
3.4 Available Scheduling Tools
3.5 Available Real-Time Operating Systems
3.6 Historical Perspective and Related Work
3.7 Summary
4 Model Checking of Finite-State Systems
4.1 System Specification
4.2 Clarke-Emerson-Sistla Model Checker
4.3 Extensions to CTL
4.4 Applications
4.5 Complete CTL Model Checker in C
4.6 Symbolic Model Checking
4.7 Real-Time CTL
4.8 Available Tools
4.9 Historical Perspective and Related Work
4.10 Summary
5 Visual Formalism, Statecharts, And Statemate
5.1 Statecharts
5.2 Activity-Charts
5.3 Module-Charts
5.4 Statemate
5.5 Available Tools
5.6 Historical Perspective and Related Work
5.7 Summary
6 Real-Time Logic, Graph-Theoretic Analysis, and Modechart
6.1 Specification and Safety Assertions
6.2 Event-Action Model
6.3 Real-Time Logic
6.4 Restricted RTL Formulas
6.5 Checking for Unsatisfiability
6.6 Efficient Unsatisfiability Check
6.7 Industrial Example: NASA X-38 Crew Return Vehicle
6.8 Modechart Specification Language
6.9 Verifying Timing Properties of Modechart Specifications
6.10 Available Tools
6.11 Historical Perspective and Related Work
6.12 Summary
7 Verification Using Timed Automata
7.1 Lynch-Vaandrager Automata-Theoretic Approach
7.2 Alur-Dill Automata-Theoretic Approach
7.3 Alur-Dill Region Automaton and Verification
7.4 Available Tools
7.5 Historical Perspective and Related Work
7.6 Summary
8 Timed Petri Nets
8.1 Untimed Petri Nets
8.2 Petri Nets with Time Extensions
8.3 Time ER Nets
8.4 Properties of High-Level Petri Nets
8.5 Berthomieu-Diaz Analysis Algorithm for TPNs
8.6 Milano Group's Approach to HLTPN Analysis
8.7 Practicality: Available Tools
8.8 Historical Perspective and Related Work
8.9 Summary
9 Process Algebra
9.1 Untimed Process Algebras
9.2 Milner's Calculus of Communicating Systems
9.3 Timed Process Algebras
9.4 Algebra of Communicating Shared Resources
9.5 Analysis and Verification
9.6 Relationships to Other Approaches
9.7 Available Tools
9.8 Historical Perspective and Related Work
9.9 Summary
10 Design And Analysis of Propositional-Logic Rule-Based Systems
10.1 Real-Time Decision Systems
10.2 Real-Time Expert Systems
10.3 Propositional-Logic Rule-Based Programs: the EQL Language
10.4 State-Space Representation
10.5 Computer-Aided Design Tools
10.6 The Analysis Problem
10.7 Industrial Example: Analysis of the Cryogenic Hydrogen Pressure Malfunction Procedure of the Space Shuttle Vehicle Pressure Control System
10.8 The Synthesis Problem
10.9 Specifying Termination Conditions in Estella
10.10 Two Industrial Examples
10.11 The Estella-General Analysis Tool
10.12 Quantitative Timing Analysis Algorithms
10.13 Historical Perspective and Related Work
10.14 Summary
11 Timing Analysis Of Predicate-Logic Rule-Based Systems
11.1 The OPS5 Language
11.2 Cheng-Tsai Timing Analysis Methodology
11.3 Cheng-Chen Timing Analysis Methodology
11.4 Historical Perspective and Related Work
11.5 Summary
12 Optimization of
Go to:Top of Page