Verification of Digital and Hybrid Systems

This book grew out of a NATO Advanced Study Institute summer school that was held in Antalya, TUrkey from 26 May to 6 June 1997. The purpose of the summer school was to expose recent advances in the formal verification of systems composed of both logical and continuous time components. The course was structured in two parts. The first part covered theorem-proving, system automaton models, logics, tools, and complexity of verification. The second part covered modeling and verification of hybrid systems, i. e. , systems composed of a discrete event part and a continuous time part that interact with each other in novel ways. Along with advances in microelectronics, methods to design and build logical systems have grown progressively complex. One way to tackle the problem of ensuring the error-free operation of digital or hybrid systems is through the use of formal techniques. The exercise of comparing the formal specification of a logical system namely, what it is supposed to do to its formal operational description-what it actually does!-in an automated or semi-automated manner is called verification. Verification can be performed in an after-the-fact manner, meaning that after a system is already designed, its specification and operational description are regenerated or modified, if necessary, to match the verification tool at hand and the consistency check is carried out.

I. Discrete Event System Verification.- 1. Overview of Verification.- 1.Bugs.- 1.1 Concurrency bugs.- 1.2 An example.- 1.3 A real-life concurrency bug.- 2.The Mathematical Approach.- 2.1 Easy objections.- 2.2 The real objection.- 3. A Selective History.- 3.1 Early 1960’s.- 3.2 Late 1960’s.- 3.3 1970’s.- 3.4 Late 1960’s.- 3.5 1980’s.- 3.6 Late 1980’s.- 3.7 1990’s.- 2. General Purpose Theorem Proving Methods in the Verification of Digital Hardware and Software.- 1. Introduction.- 1.1 Formal models.- 1.2 Lessons.- 1.3 A spectrum of choices.- 1.4 Outline of this presentation.- 2. The ACL2 Theorem Prover.- 2.1 NQTHM: the Boyer-Moore System.- 2.2 A simple example of ACL2.- 2.3 A more interesting example.- 2.4 Five key ideas in ACL2.- 3. Using ACL2 to Model Digital Systems.- 4. Industrial Scale Applications of ACL2.- 4.1 AMD floating point arithmetic.- 4.2 Motorola CAP digital signal processor.- 4.3 Summary of ACL2 applications.- 5. Other General-Purpose Systems.- 5.1 HOL.- 5.2 PVS.- 6. Conclusion.- 3. Temporal Logic and Model Checking.- 1. Reactive Systems and Temporal Properties.- 1.1 Example: The alternating bit protocol.- 1.2 Temporal properties.- 1.3 Formalizing temporal properties.- 1.4 Model theory for temporal logic.- 1.5 Proofs in temporal logic.- 2. Model Checking (Clarke/Emerson, Queille/Sifakis).- 2.1 Example: Modeling a protocol in CSP (Hoare).- 3. Branching Time and CTL Model Checking.- 3.1 CTL model checking.- 3.2 Example: The ABP revisited.- 4. Expressiveness Issues.- 4.1 Linear vs. branching time.- 4.2 Data independence.- 5. Summary.- 4. Model Checking Using Automata Theory.- 1. ?-Automata.- 2. Specification Using ?-Automata.- 3. Operations on BÜchi Automata.- 4. Checking Emptiness.- 5. Other Acceptance Conditions.- 6. Translating LTL into Automata.- 6.1 Linear temporal logic.- 6.2 The translation algorithm.- 6.3 Improvements to the algorithm.- 7. The Expressive Power of BÜchi Automata.- 8. The Complexity of LTL Model Checking.- 5. Complexity Issues in Automata Theoretic Verification.- 1. Introduction.- 1.1 About u;-automata based verification.- 2. About the COSPAN Verification Tool.- 2.1 Introduction.- 2.2 Modeling hardware.- 2.3 Specification and proof.- 2.4 Handling the complexity theoretic lowerbounds.- 3. The Theoretical Foundations: Boolean Algebra, Languages, and Selection-Resolution.- 3.1 Boolean algebra, automata and languages.- 3.2 Some words about Boolean algebras.- 3.3 L-automaton and L-process.- 3.4 Selection/resolution model.- 3.5 Verification based on L-processes and L-automata.- 4. Reduction Methodologies.- 4.1 Homomorphic reduction and refinement based topdown methodology.- 4.2 Inductive abstraction.- 6. Symbolic Model Checking.- 1. Introduction.- 2. Binary Decision Diagrams.- 2.1 Apply algorithm.- 2.2 The quantification algorithm.- 2.3 Circuit width and OBDD size.- 2.4 Variable ordering.- 3. Representing Sets and Relations.- 3.1 Char acter ist ic functions of sets.- 3.2 Characteristic functions of relations.- 3.3 Forward and reverse image.- 3.4 Reachability analysis using OBDD’s.- 4. Fixed Point Characterization of CTL.- 4.1 Fixed points of monotonic functions.- 4.2 Characterization of EG.- 4.3 Complexity of OBDD based model checking.- 5. The SMV System.- 5.1 SMV language.- 5.2 Example - a synchronous arbiter circuit.- 5.3 Example - distributed cache coherence protocol.- 6. The Mu-calculus and Symbolic Model Checking.- 6.1 Propositional mu-calculus.- 6.2 Mu-calculus and CTL.- 6.3 Relational mu-calculus and symbolic model checking.- 7. Summary.- 7. Compositional Systems and Methods.- 1. Introduction.- 2. A Framework for Compositional Minimization.- 2.1 Framework.- 2.2 An example framework.- 2.3 Application: Decoupled processor Controller.- 2.4 Hierarchical minimization.- 3. Assume/Guarantee Style Reasoning.- 3.1 Frameworkk.- 3.2 An example framework.- 3.3 Why not ordinary CTL?.- 3.4 Application example - CPU Controller revisitedn.- 4. Conclusion.- 8. Symmetry and Model Checking.- 1. Symmetry and Model Checking.- 1.1 Permutations.- 1.2 Permutation groups.- 1.3 Symmetry in Kripke models.- 1.4 Reduced models.- 1.5 Checking CTL* formulas.- 2. Murphi - A Practical Approach to Symmetry Reductions.- 2.1 The Murphi language.- 2.2 Scalar sets.- 2.3 Cache protocol example.- 2.4 Data Saturation.- 3. Summary.- 9. Partial Order Reductions.- 1. Introduction.- 2. Modeling Concurrent Systems.- 2.1 State spaces of concurrent Systems.- 3. Stuttering Equivalence.- 3.1 Syntax and semantics of CTL*, CTL and LTL.- 4. Verification Using Representatives.- 4.1 Ample sub-state-spaces.- 5. Partial Order Reduction for Linear Specifications.- 5.1 The ample-sets reduction method.- 6. Reduction for Branching TL and Process Algebras.- 6.1 Behavioral equivalences.- 6.2 Correctness of the algorithm.- 7. Implementation Issues.- 8. Reducing the Visibility Constraint.- 9. Static Partial Order Reduction.- 10. Probabilistic Model Checking: Formalisms and Algorithms for Discrete and Real-time Systems.- 1. Introduction.- 2. Preliminaries.- 2.1 Stochastic processes.- 3. Description Formalisms.- 3.1 Discrete-time probabilistic Systems.- 3.2 Discrete-time probabilistic specifications.- 4. Complexity Results.- 4.1 Verification problems.- 4.2 Results for Markov chains.- 4.3 Results for concurrent Markov chains.- 5. Algorithms.- 5.1 Computing satisfaction probabilities for Markov chains.- 5.2 Checking emptiness for concurrent Markov chains.- 6. Extensions for ETL and PCTL*.- 6.1 Extended temporal logic.- 6.2 Probabilistic computation tree logic.- 7. Description Formalisms.- 7.1 Real-time probabilistic Systems.- 7.2 Real-time probabilistic specifications.- 8. Complexity Results.- 8.1 Verification problems.- 8.2 Results.- 10. Conclusions.- 11. Formal Verification in a Commercial Setting.- 1. Introduction.- 2. Paradigms.- 3. Reduction.- 4. Interfaces.- 5. Support.- 6. Examples of Practice.- 7. Future.- II. Hybrid Systems: Modeling and Verification.- 12. Timed Automata.- 1. Modeling.- 2. Reachability Analysis.- 3. Automata-Theoretic Verification.- 3.1 Verification via Automata Emptiness.- 3.2 Theory of Timed Languages.- 4. Tools and Applications.- 5. Discussion.- 13. The Theory of Hybrid Automata.- 1. Hybrid Automata.- 1.1 Syntax.- 1.2 Safe Semantics.- 1.3 Live Semantics.- 1.4 Composition.- 2. On the Trace Languages of Hybrid Automata.- 2.1 Verification Tasks.- 2.2 Rectangular Automata.- 2.3 Verification Results.- 3. On the State Spaces of Hybrid Automata.- 3.1 Symbolic Analysis of Transition Systems.- 3.2 Linear Hybrid Automata.- 3.3 Bisimilarity and Similarity Relations.- 3.4 Computation Tree Logics.- 14. On the Composition of Hybrid Systems.- 1. Introduction.- 3.1 Symbolic Analysis of Transition Systems.- 2.1 Discrete Systems.- 2.2 Hybrid extension of SA.- 2.3 Comparing hybrid actions.- 3. Choice Operators.- 3.1 Priority choice.- 3.2 Consensual choice.- 4. Parallel composition.- 4.1 Extending parallel composition from untimed to hybrid Systems.- 4.2 Synchronization modes of hybrid actions.- 5. Applications.- 6. Discussion.- 15. Reach Set Computation Using Optimal Control.- 1. Introduction.- 2. Convex Reach Set Function.- 3. Maximum principle.- 4. Concluding remarks.- 16. Control for a Class of Hybrid Systems.- 1. Introduction.- 2. Example of Conveyor Belts.- 3. Modeling of hybrid Systems.- 3.1 Definitions.- 3.2 Subclasses of the Class of Hybrid Control Systems.- 3.3 Realization of Hybrid Systems.- 4. Control of Hybrid Systems.- 4.1 Problem Formulation.- 4.2 Example.- 4.3 Control Synthesis for a Special Class of Systems.- 4.4 Reachability Problems.- 5. Concluding Remarks.- 17. The SHIFT Programming Language and Run-time System for Dynamic Networks of Hybrid Automata.- 1. Introduction.- 1.1 Related Work.- 2. The SHIFT Language.- 3. The SHIFT Model.- 3.1 Type Description.- 3.2 Component Description.- 3.3 World Description..- 3.4 World Semantics.- 4. The Particle Example.- 4.1 The Particle Type.- 4.2 The Source Type.- 4.3 The Monitor Type.- 4.4 Global Variables.- 5. Conclusion.- 18. The Teja System for Real-Time Dynamic Event Management.- 1. Introduction.- 1.1 Enterprise Systems.- 1.2 Embedded Systems.- 1.3 Integrated Management.- 1.4 Performance.- 1.5 Tools Interfaces.- 2. The Teja Model.- 2.1 Basic Concepts.- 2.2 The Component Model.- 2.3 Event Model.- 2.4 Alert Model.- 2.5 Inheritance and Other Object-Oriented Features.- 2.6 Server Behavior.- 2.7 Client Behavior.- 19. Automated Highway Systems: an Example of Hierarchical Control.- 1. Background.- 2. AHS design space.- 3. A control architecture.- 4. Design and verification of control.- 5. Remarks on layered control architectures.