Ebook: 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.

---

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.

---

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.
Content:
Front Matter....Pages I-XVIII
Front Matter....Pages 1-1
Overview of Verification....Pages 3-13
General Purpose Theorem Proving Methods in the Verification of Digital Hardware and Software....Pages 14-35
Temporal Logic and Model Checking....Pages 36-54
Model Checking Using Automata Theory....Pages 55-79
Complexity Issues in Automata Theoretic Verification....Pages 80-116
Symbolic Model Checking....Pages 117-137
Compositional Systems and Methods....Pages 138-151
Symmetry and Model Checking....Pages 152-162
Partial Order Reductions....Pages 163-182
Probabilistic Model Checking: Formalisms and Algorithms for Discrete and Real-time Systems....Pages 183-219
Formal Verification in a Commercial Settings....Pages 220-230
Front Matter....Pages 231-231
Timed Automata....Pages 233-264
The Theory of Hybrid Automata....Pages 265-292
On the Composition of Hybrid Systems....Pages 293-322
Reach Set Computation Using Optimal Control....Pages 323-331
Control for a Class of Hybrid Systems....Pages 332-354
The SHIFT Programming Language and Run-time System for Dynamic Networks of Hybrid Automata....Pages 355-371
The Teja System for Real-Time Dynamic Event Management....Pages 372-390
Automated Highway Systems: an Example of Hierarchical Control....Pages 391-402
Back Matter....Pages 403-406

---

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.
Content:
Front Matter....Pages I-XVIII
Front Matter....Pages 1-1
Overview of Verification....Pages 3-13
General Purpose Theorem Proving Methods in the Verification of Digital Hardware and Software....Pages 14-35
Temporal Logic and Model Checking....Pages 36-54
Model Checking Using Automata Theory....Pages 55-79
Complexity Issues in Automata Theoretic Verification....Pages 80-116
Symbolic Model Checking....Pages 117-137
Compositional Systems and Methods....Pages 138-151
Symmetry and Model Checking....Pages 152-162
Partial Order Reductions....Pages 163-182
Probabilistic Model Checking: Formalisms and Algorithms for Discrete and Real-time Systems....Pages 183-219
Formal Verification in a Commercial Settings....Pages 220-230
Front Matter....Pages 231-231
Timed Automata....Pages 233-264
The Theory of Hybrid Automata....Pages 265-292
On the Composition of Hybrid Systems....Pages 293-322
Reach Set Computation Using Optimal Control....Pages 323-331
Control for a Class of Hybrid Systems....Pages 332-354
The SHIFT Programming Language and Run-time System for Dynamic Networks of Hybrid Automata....Pages 355-371
The Teja System for Real-Time Dynamic Event Management....Pages 372-390
Automated Highway Systems: an Example of Hierarchical Control....Pages 391-402
Back Matter....Pages 403-406
....