© 2000

Verification of Digital and Hybrid Systems

  • M. Kemal Inan
  • Robert P. Kurshan

Part of the NATO ASI Series book series (volume 170)

Table of contents

  1. Front Matter
    Pages I-XVIII
  2. Discrete Event System Verification

    1. Front Matter
      Pages 1-1
    2. Kenneth McMillan
      Pages 3-13
    3. Kenneth L. McMillan
      Pages 36-54
    4. Sandeep K. Shukla
      Pages 55-79
    5. Kenneth L. McMillan
      Pages 117-137
    6. Kenneth L. McMillan
      Pages 138-151
    7. Kenneth McMillan
      Pages 152-162
    8. Doron Peled
      Pages 163-182
    9. R. P. Kurshan
      Pages 220-230
  3. Hybrid Systems: Modeling and Verification

    1. Front Matter
      Pages 231-231
    2. Rajeev Alur
      Pages 233-264
    3. Thomas A. Henzinger
      Pages 265-292
    4. Sébastien Bornot, Joseph Sifakis
      Pages 293-322
    5. Pravin Varaiya
      Pages 323-331
    6. Jan H. van Schuppen
      Pages 332-354
    7. Akash Deshpande, Aleks Göllü, Luigi Semenzato
      Pages 355-371

About this book


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.


algorithms automata automata theory complexity control design hardware heuristics language modeling programming programming language proving software verification

Editors and affiliations

  • M. Kemal Inan
    • 1
  • Robert P. Kurshan
    • 2
  1. 1.Faculty of Engineering and Natural Sciences Sabanci UniversityTuzla-IstanbulTurkey
  2. 2.Bell Laboratories600 Mountain AvenueUSA

Bibliographic information

Industry Sectors
IT & Software