## Verification of Digital and Hybrid SystemsThis 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. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Overview of Verification | 3 |

General Purpose Theorem Proving Methods | 14 |

Industrial Scale Applications of ACL2 | 29 |

Copyright | |

34 other sections not shown

### Other editions - View all

Verification of Digital and Hybrid Systems M. Kemal Inan,Robert P. Kurshan No preview available - 2011 |

### Common terms and phrases

abstraction accepting ACL2 algorithm Alur automaton H behavior belt Biichi automaton bisimulation Boolean algebra clock zone complexity component composition computation tree logic Computer Science concurrent condition COSPAN defined Definition denote deterministic discrete edge EQUAL REV equivalence relation event example finite set formal formal verification formula function graph homomorphism hybrid actions hybrid automata hybrid control system hybrid systems infinite initial input L-process labeled labeled transition system language Lemma linear hybrid LNCS Markov chain model checking Moore machine Muller automaton node Notes in Computer operators output partial order partial order reduction path predicate probabilistic proof protocol PSPACE reachability problem real-time systems rectangular reduction region automaton satisfies semantics sequence specification Springer-Verlag subset switch symbolic synchronization T.A. Henzinger Teja temporal logic Theorem theory time-abstract tool transition relation transition system tray tuple variables vehicles verification w-automata