Verification of Digital and Hybrid Systems

ISBN-13: 9783642640520 / Angielski / Miękka / 2011 / 405 str.

M. Kemal Inan; Robert P. Kurshan

Opis

This state-of-the-art tutorial overview of computer-aided verification, hybrid systems, and publicly available tools for design and verification is based on a NATO workshop. It has two parts. Part 1 addresses the basics of computer-aided verification of discrete event systems from two perspectives: automated theorem proving and model checking. In model checking, the essential problem of computational complexity is addressed, and the basic heuristics for dealing with this problem are presented. Part 2 formulates and classifies hybrid systems that capture continuous dynamics interacting with activated discrete event interruptions modeled by automata, and presents and discusses properties relevant to design and verification such as decidability, complexity, and expressibility for computer tools. The theory is illustrated with real-life examples. One novel and industrially relevant example is that of an intelligent highway transport system.

Spis treści

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.