PREFACE
This text is based on two rich sources: (1) materials in lecture notes I taught to senior and graduate-level computer science and electrical engineering students at Rice University and at the University of Houston, and (2) my research in the area of timing analysis and verification of real-time systems since the late 1980s, especially in the emerging area of embedded rule-based systems. Condensed forms of key concepts appearing in this text have been presented in my tutorials and seminars at many major international conferences. The focus is on the formal analysis and verification of real-time systems. The text is self-contained in that it includes a presentation of basic real-time scheduling algorithms and schedulability analysis as well as a description of the necessary background in logic and automata theory for understanding the more advanced materials. It provides a clear presentation of the concepts underlying the formal methods for real-time systems design.
Many of the systems and devices used in our modern society must provide a response that is both correct and timely. More and more computer systems are built as integral parts of many of these systems to monitor and control their functions and operations. These embedded systems often operate in environments where safety is a major concern. Examples range from simple systems such as climate-control systems, toasters, and rice cookers to highly complex systems such as airplanes and space shuttles. Other examples include hospital patient-monitoring devices and braking controllers in automobiles. Toward the goal of ensuring that these safety-critical systems operate as specified by the design and safety requirements, we have to develop sound methodologies and apply the corresponding tools to analyze and verify that these systems meet their specifications.
Much has been written in the area of formal analysis and verification of realtime systems in the form of technical papers that assume an advanced mathematical
xiii
xiv PREFACE
background on the part of the reader. Many of these presentations tend to be narrow in their coverage and many are model, architecture, or implementation dependent. Although they are timely and useful disseminations of state-of-the-art results, often there is little unifying discussion or foundation linking or relating the different results, making it difficult to make use of the results in practice. They are usually written in a formal manner with extensive notation and proofs, and with the assumption that the reader is a knowledgeable researcher in the same field. Since research results must be reported in a timely manner in the scientific field, authors of these papers do not have the time and space to show extensive examples or to provide a more tutorial perspective. Several books are available on the subject of analysis and verification of real-time systems, but they are basically collections of papers in their original form, sometimes with very brief, additional introductions to the papers.
Therefore, the purpose of this text is to make the most significant of these state- of-the-art materials accessible to upper-division undergraduates (juniors and seniors) and first-year graduates while still serving as a resourceful reference for more advanced practitioners and researchers by providing an extensive bibliography and pointers to more detailed papers on selected topics. This text is also a more unified treatment of the different approaches to analysis and verification. It compares these approaches and relates one approach to another so that the reader can decide when to use which approach or combination of approaches. The text does not attempt to be comprehensive but does present the most significant trends in the field. Thus, it also serves as a motivating source to generate interest in the area in order to tackle the many difficult problems awaiting correct or efficient solutions.
EXAMPLES
The text describes the application of the presented techniques and tools to a variety of industrial and toy examples. For easy reference, we list the major examples:
•Automatic air conditioning and heating unit (chapter 2)
•Simplified automobile control (chapters 2, 4, 7)
•Smart traffic light system for a traffic intersection (chapters 2, 8)
•Railroad crossing (chapters 4, 6)
•Mutual exclusion problem for processes (chapter 5)
•NASA X-38 Crew Return Vehicle avionics (chapter 6)
•NASA Mars Odyssey Orbiter (chapter 5)
•Message sending and acknowledgment (chapter 7)
•Airport radar system (chapter 9)
•Object detection (chapter 9)
•Space Shuttle Cryogenic Hydrogen Pressure Malfunction Procedure (chapter 10)
•Fuel cell expert system (FCE) (chapter 10)
PREFACE xv
•Integrated status assessment expert system (ISA) (chapters 10, 11, 12)
•Seat assignment (chapter 11)
•Analysis of 2D line-drawing representation of 3D objects (chapter 11)
•Space Shuttle Orbital Maneuvering and Reaction Control Systems’ Valve and Switch Classification Expert System (OMS) (chapter 11)
TEXT OUTLINE
Common to every chapter is a description of the available design, analysis, and verification tools; a section on historical perspective and related work; a summary; and a set of exercises.
Chapter 1 introduces real-time systems, defines the notion of time and how to measure it, and provides a synopsis of several analysis techniques, including simulation, testing, verification, and run-time monitoring. It also gives pointers to useful resources in the study and design of real-time systems.
Chapter 2 describes the analysis and verification of non-real-time systems using symbolic logic and automata-theoretic approaches. It covers topics in propositional logic, proving satisfiability using the resolution procedure, predicate logic, prenex normal forms, Skolem standard forms, proving unsatisfiability of a clause set with Herbrand’s procedure and the resolution procedure, languages and their representations, finite automata, and the specification and verification of untimed systems.
Chapter 3 presents real-time scheduling and schedulability analysis, covering topics in computation time prediction, uniprocessor scheduling, scheduling preemptable and independent tasks, fixed-priority schedulers, rate-monotonic and deadlinemonotonic algorithms, dynamic-priority schedulers, earliest-deadline-first (EDF) algorithm, least-laxity-first (LL) algorithm, scheduling nonpreemptable sporadic tasks, nonpreemptable tasks with precedence constraints, periodic tasks with precedence constraints, communicating periodic tasks, deterministic rendezvous model, periodic tasks with critical sections, kernelized monitor model, multiprocessor scheduling, schedule representations, scheduling game board, sufficient conditions for conflictfree task sets, scheduling periodic tasks on a multiprocessor, PERTS, PerfoRMAx, TimeWiz, and real-time operating systems (RTOSs).
Chapter 4 describes model checking of finite-state systems. Topics covered include system specification, Clarke–Emerson–Sistla model checker, CTL, complete CTL model checker in C, symbolic model checking, binary decision diagrams, realtime CTL, minimum and maximum delays, minimum and maximum number of condition occurrences, and state graphs with non-unit transition time.
Chapter 5 presents visual formalism, Statecharts, and Statemate, covering basic Statecharts features, including OR-decomposition, AND-decomposition, delays and timeouts, condition and selection entrances, and unclustering. It also describes activity-charts, module-charts, Statechart semantics, and code executions and analysis.
Chapter 6 describes real-time logic (RTL), graph-theoretic analysis, and Modechart, covering specification and safety assertions, event-action model, restricted
xvi PREFACE
RTL formulas, constraint-graph construction, unsatisfiability check, analysis complexity and optimization, NASA X-38 Crew Return Vehicle X-38 Avionics Architecture, Modechart, verification of timing properties of Modechart specifications, system computations, and computation graphs. It presents techniques for finding the minimum and maximum distance between endpoints, and exclusion and inclusion of endpoint and interval.
Chapter 7 describes verification using timed automata. Topics covered include Lynch–Vaandrager automata-theoretic approach, timed executions, timed traces, composition of timed automata, MMT automata, proving time bounds with simulations, Alur–Dill automata-theoretic approach, untimed traces, timed traces, Alur–Dill timed automata, Alur–Dill region automaton and verification, and clock regions.
Chapter 8 presents untimed Petri nets and time/timed Petri nets. Topics covered include conditions for firing enabled transitions, environment/relationship nets, high-level timed Petri nets (HLTPNs), time ER nets, strong and weak time models, properties of high-level Petri Nets, Berthomieu–Diaz analysis algorithm for TPNs, determining fireability of transitions, deriving reachable classes, Milano Group’s approach to HLTPN analysis, and facilitating analysis with TRIO.
Chapter 9 presents process-algebraic approaches to verification, covering untimed process algebra, Milner’s Calculus of Communicating Systems (CCS), direct equivalence of behavior programs, congruence of behavior programs, equivalence relations, bisimulation, timed process algebras, Algebra of Communicating Shared Resources (ACSR), syntax of ACSR and semantics of ACSR, operational rules, analysis, and VERSA.
Chapter 10 describes the design and timing analysis of propositional-logic rulebased systems. Topics covered include real-time decision systems, real-time expert systems, EQL language, state space representation, computer-aided design tools, response time analysis problem, finite domains, special form, general analysis strategy, synthesis problem, time complexity of scheduling equational rule-based programs, method of Lagrange multipliers, specifying termination conditions in Estella, behavioral constraint assertions, syntax and semantics of Estella, specifying Special Forms with Estella, context-free grammar for Estella, Estella-General Analysis Tool, selecting independent rule set, constructing and checking the dependency graph, checking compatibility conditions, checking cycle-breaking conditions, quantitative timing analysis algorithms, mutual exclusiveness and compatibility, high-level dependency graph, and rule-dependency graph.
Chapter 11 presents the timing analysis of predicate-logic rule-based systems, covering the OPS5 language, Rete network, Cheng–Tsai timing analysis methodology, static analysis of control paths in OPS5, termination analysis, termination detection, enabling conditions of a cycle, prevention of cycles, program refinement, redundant conditions, redundant extra rules, timing analysis, prediction of the number of rule firings, WM generation, maximizing matching time, maximizing rule firings, complexity and space reduction, ordering of the initial WMEs, Cheng–Chen timing analysis methodology, classification of OPS5 programs, maximal numbers of new matching WMEs number of comparisons, the class of cyclic programs, and removing cycles with programmer’s help.
PREFACE xvii
Chapter 12 describes the optimization of rule-based systems. Topics covered include execution model of a real-time decision system based on a state space representation, several optimization algorithms, derivation of an optimized state space graph, synthesis of an optimized EQL(B) program, EQL(B) programs without cycles, EQL(B) programs with cycles, qualitative comparison of optimization methods, constraints over EQL language required by optimization, and optimization of other real-time rule-based systems.
ACKNOWLEDGMENTS
I would like to express my sincere thanks to editor Andrew J. Smith, who first inivited me to embark on this textbook project, to the current senior editor Philip Meyler, who is very supportive and flexible with deadlines, to the anonymous reviewers for providing constructive comments, to my Ph.D. student Mark T.-I. Huang for drawing many of the figures, and to associate managing editor Angioline Loredo, Kirsten Rohsted, and the editorial staff for professional editing. My family and friends have provided continuous encouragement and support for which I am greatly indebted.
ALBERT M. K. CHENG
Houston, TX