Verification of Digital and Hybrid Systems

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.