Overview

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.

Full Product Details

Author:   M. Kemal Inan ,  Robert P. Kurshan
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Edition:   Softcover reprint of the original 1st ed. 2000
Volume:   170
Dimensions:   Width: 15.50cm , Height: 2.20cm , Length: 23.50cm
Weight:   0.645kg
ISBN:  

9783642640520

ISBN 10:   3642640524
Pages:   405
Publication Date:   30 September 2011
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   Manufactured on demand  
We will order this item for you from a manufactured on demand supplier.

Table of Contents

I. Discrete Event System Verification.- 1. Overview of Verification.- 2. General Purpose Theorem Proving Methods in the Verification of Digital Hardware and Software.- 3. Temporal Logic and Model Checking.- 4. Model Checking Using Automata Theory.- 5. Complexity Issues in Automata Theoretic Verification.- 6. Symbolic Model Checking.- 7. Compositional Systems and Methods.- 8. Symmetry and Model Checking.- 9. Partial Order Reductions.- 10. Probabilistic Model Checking: Formalisms and Algorithms for Discrete and Real-time Systems.- 11. Formal Verification in a Commercial Setting.- II. Hybrid Systems: Modeling and Verification.- 12. Timed Automata.- 13. The Theory of Hybrid Automata.- 14. On the Composition of Hybrid Systems.- 15. Reach Set Computation Using Optimal Control.- 16. Control for a Class of Hybrid Systems.- 17. The SHIFT Programming Language and Run-time System for Dynamic Networks of Hybrid Automata.- 18. The Teja System for Real-Time Dynamic Event Management.- 19. Automated Highway Systems: an Example of Hierarchical Control.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions