Efficient Decompositional Model Checking for Regular Timing Diagrams

  • Nina Amla
  • E. Allen Emerson
  • Kedar S. Namjoshi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


Timing diagrams are widely used in industrial practice to express precedence and timing relationships amongst a collection of signals. This graphical notation is often more convenient than the use of temporal logic or automata. We introduce a class of timing diagrams called Regular Timing Diagrams (RTD’s). RTD’s have a precise syntax, and a formal semantics that is simple and corresponds to common usage. Moreover, RTD’s have an inherent compositional structure, which is exploited to construct an efficient algorithm for model checking a RTD with respect to a system description. The algorithm has time complexity that is linear in the system size and a small polynomial in the representation of the diagram. The algorithm can be easily used with symbolic (BDDbased) model checkers. We illustrate the workings of our algorithm with the verification of a simple master-slave system.


Model Check Temporal Logic Regular Language Timing Diagram Sequential Dependency 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    C. Antoine and B. Le Goff. Timing Diagrams for Writing and Checking Logical and Behavioral Properties of Integrated Systems. In Correct Hardware Design Methodologies. Elsevier Sciences Publishers, 1992.Google Scholar
  2. 2.
    G. Borriello. Formalized Timing Diagrams. In EDAC92. IEEE Comput. Soc. Press, 1992.Google Scholar
  3. 3.
    R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS. In FMCAD, 1996.Google Scholar
  4. 4.
    V. Cingel. A Graph-based Method for Timing Diagrams Representation and Verification. In Correct Hardware Design and Verification Methods. Springer Verlag, 1993.Google Scholar
  5. 5.
    E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In Workshop on Logics of Programs, volume 131. Springer Verlag, 1981.Google Scholar
  6. 6.
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic. ACM Transactions on Programming Languages and Systems, 8(2), 1986.Google Scholar
  7. 7.
    W. Damm and J. Helbig. Linking Visual Formalisms: A Compositional proof System for Statecharts cased on Symbolic Timing Diagrams. In E. R. Olderog, editor, Programming Concepts, Methods and Calculi. Elsevier Science B. V. (North Holland), 1994.Google Scholar
  8. 8.
    W. Damm, H. Hunger, P. Kelb, and R. Schlör. Using Graphical Specification Languages and Symbolic Model Checking in the Verification of a Production Cell. In C. Lewerentz and T. Lindner, editors, Formal Development of Reactive Systems. Case Study Production Cell, LNCS 891. Springer Verlag, 1994.Google Scholar
  9. 9.
    W. Damm, B. Josko, and Rainer Schlör. Specification and Verification of VHDLbased System-level Hardware Designs. In Egon Borger, editor, Specificatio and Validation Methods. Oxford University Press, 1994.Google Scholar
  10. 10.
    K. Feyerabend. Real-time Symbolic Timing Diagrams. Technical report, Department of Computer Science, Oldenburg University, September 1994.Google Scholar
  11. 11.
    K. Feyerabend and B. Josko. A Visual Formalism for Real Time Requirement Specifications. In AMAST Workshop on Real-time systems and Concurrent and Distributed Software. Springer Verlag, 1997.Google Scholar
  12. 12.
    K. Feyerabend and R. Schlör. Hardware synthesis from requirement specifications. In EURO-DAC'96 with EURO-VHDL'96. IEEE Computer Society Press, September 1996.Google Scholar
  13. 13.
    K. Fisler. A Unified Approach to Hardware Verification Through a Heterogeneous Logic of Design Diagrams. PhD thesis, Computer Science Department, Indiana University, August 1996.Google Scholar
  14. 14.
    K. Fisler. Containment of Regular Languages in Non-Regular Timing Diagrams Languages is Decidable. In CAV. Springer Verlag, 1997.Google Scholar
  15. 15.
    W. Grass, C. Grobe, S. Lenk, W. Tiedemann, C. D. Kloos, A. Marin, and T. Robles. Transformation of Timing Diagram Specifications into VHDL Code. In Conference on Hardware Description Languages, 1995.Google Scholar
  16. 16.
    J. Helbig, R. Schlör, W. Damm, G. Doehmen, and P. Kelb. VHDL/S-I ntegrating Statecharts, Timing diagrams, and VHDL. Microprocessing and Microprogramming, 1996.Google Scholar
  17. 17.
    F. Jin and E. Cerny. Verification of Real-Time Controllers against Timing Diagram Specifications using Constraint Logic Programming. In IFIP EuroMICRO, 1998.Google Scholar
  18. 18.
    K. Khordoc and E. Cerny. Semantics and Verification of Timing Diagrams with Linear Timing Constraints. ACM Transactions on Design Automation of Electronic Systems, 3(1), 1998.Google Scholar
  19. 19.
    R. P. Kurshan. Computer-aided verification of coordinating processes: the Automata-theoretic approach. Princeton University Press, 1994.Google Scholar
  20. 20.
    O. Lichtenstein and A. Pnueli. Checking that Finite State Concurrent Programs satisfy their Linear Specifications. In POPL, 1985.Google Scholar
  21. 21.
    Z. Manna and A. Pnueli. Specification and Verification of Concurrent Programs by ∀-Automata. In POPL, 1987.Google Scholar
  22. 22.
    J. P. Queille and J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982.Google Scholar
  23. 23.
    Y. S.. Ramakrishna, P. M. Melliar-Smith, L. E. Moser, L. K. Dillon, and G. Kutty. Really Visual Temporal Reasoning. In Real-Time Systems Symposium. IEEE Publishers, 1993.Google Scholar
  24. 24.
    R. Schlör. A Prover for VHDL-based Hardware Design. In Conference on Hardware Description Languages, 1995.Google Scholar
  25. 25.
    A. P. Sistla, M. Vardi, and P. Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic. TCS, 49, 1987.Google Scholar
  26. 26.
    E. M. Thurner. Proving System Properties by means of Trigger-Graph and Petri Nets. In EUROCAST. Springer Verlag, 1996.Google Scholar
  27. 27.
    W. D. Tiedemann. Bus Protocol Conversion: from Timing Diagrams to State Machines. In EUROCAST. Springer Verlag, 1992.Google Scholar
  28. 28.
    M. Vardi. Verification of Concurrent Programs. In POPL, 1987.Google Scholar
  29. 29.
    M. Vardi and P. Wolper. An Automata-Theoretic approach to Automatic Program Verification. In LICS, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Nina Amla
    • 1
  • E. Allen Emerson
    • 1
  • Kedar S. Namjoshi
    • 2
  1. 1.Department of Computer SciencesUniversity of Texas at AustinUSA
  2. 2.Bell LaboratoriesLucent TechnologiesUSA

Personalised recommendations