Verification of Digital and Hybrid Systems by M. Kemal InanVerification of Digital and Hybrid Systems by M. Kemal Inan

Verification of Digital and Hybrid Systems

byM. Kemal InanEditorRobert P. Kurshan

Paperback | September 30, 2011

Pricing and Purchase Info

$181.71 online 
$219.50 list price save 17%
Earn 909 plum® points

Prices and offers may vary in store


In stock online

Ships free on orders over $25

Not available in stores


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.
Title:Verification of Digital and Hybrid SystemsFormat:PaperbackDimensions:405 pages, 23.5 × 15.5 × 0.01 inPublished:September 30, 2011Publisher:Springer-Verlag/Sci-Tech/TradeLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:3642640524

ISBN - 13:9783642640520

Look for similar items by category:


Table of Contents

Part I: Overview of Verification.- General Purpose Theorem Proving Methods in the Verification of Digital Hardware and Software.- Temporal Logic and Model Checking.- Model Checking Using Automata Theory.- Complexity Issues in Automata Theoretic Verification.- Symbolic Model Checking.- Compositional Systems and Methods.- Symmetry and Model Checking.- Partial Order Reductions.- Probabilistic Model Checking: Formalisms and Algorithms for Discrete and Real-Time Systems.- Formal Verification in a Commercial Setting.- Part II: Timed Automata.- The Theory of Hybrid Automata.- On the Composition of Hybrid Systems.- Reach Set Computation Using Optimal Control.- Control for a Class of Hybrid Systems.- The SHIFT Programming Language and Run-Time System for Dynamic Networks of Hybrid Automata.- The Teja System for Real-Time Dynamic Event Management.- Automated Highway Systems: an Example of Hierarchical Control.