Advertisement

Visual Specifications for Modular Reasoning about Asynchronous Systems

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

Abstract

We propose a framework that closely ties together visual specification and modular reasoning of asynchronous systems. The basis of the framework is a new notation, called Modular Timing Diagrams (MTD’s), for specifying the universal properties about causality and timing of events in an asynchronous system. MTD’s are complementary in nature to Message Sequence Charts, that are typically used to specify existential properties. Our framework includes two algorithms for formal reasoning withMTD’s. The first is an efficient polynomial-time model checking algorithm. The second is an algorithm for automatically generating an assume-guarantee partitioning of an MTD, that exploits its inherent decompositional structure. We show how to use this decomposition for modular reasoning withMTD properties in conjunction with an asynchronous compositional reasoning rule. To illustrate the notation and our method, we describe a case study where we specified telephony features, suchas call forwarding withMTD’s, and verified these properties on an asynchronous telephony model. The compositional reasoning methods led to savings of 15%-80% in verification times, and comparable savings in space.

Keywords

Linear Temporal Logic Timing Diagram Acceptance Condition Sequential Dependency Proof Rule 
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.

References

  1. [AEKN00]
    N. Amla, E.A. Emerson, R.P. Kurshan, and K.S. Namjoshi. Model checking synchronous timing diagrams. In FMCAD, 2000.Google Scholar
  2. [AEKN01]
    N. Amla, E.A. Emerson, R.P. Kurshan, and K.S. Namjoshi. RTDT: a front-end for e.cient model checking of synchronous timing diagrams. In CAV, 2001.Google Scholar
  3. [AEN99]
    N. Amla, E.A. Emerson, and K.S. Namjoshi. Efficient decompositional model checking for regular timing diagrams. In CHARME, 1999.Google Scholar
  4. [AENT01]
    N. Amla, E.A. Emerson, K.S. Namjoshi, and R. Trefler. Assumeguarantee based compositional reasoning for synchronous timing diagrams. In TACAS, volume 2031 of LNCS, 2001.Google Scholar
  5. [AENT02]
    N. Amla, E.A. Emerson, K. Namjoshi, and R. Trefler. Compositional Reasoning for Asynchronous Systems, 2002. URL: http://-www.cs.bell-labs.com/who/kedar/publications.html.
  6. [AG01]
    R. Alur and R. Grosu. Shared variable interaction diagrams. In 16th IEEE International Conference on Automated Software Engineering, 2001.Google Scholar
  7. [AL95]
    M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. on Programming Languages and Systems (TOPLAS), May 1995.Google Scholar
  8. [AS85]
    B. Alpern and F. Schneider. Defining liveness. Information Processing Letters, 21(4), 1985.Google Scholar
  9. [AY99]
    R. Alur and M. Yannakakis. Model checking of message sequence charts. In Proc. TenthInternational Conference on Concurrency Theory, 1999.Google Scholar
  10. [DH01]
    W. Damm and D. Harel. LSCs: Breathing life into message sequence charts. Formal Methods in System Design, 19(1), 2001.Google Scholar
  11. [DJS94]
    W. Damm, B. Josko, and Rainer Schlör. Specification and verification of VHDL-based system-level hardware designs. In Egon Borger, editor, Specification and Validation Methods. Oxford University Press, 1994.Google Scholar
  12. [dRdBH+01]
    W-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, 2001.Google Scholar
  13. [dRLP97]
    W-P. de Roever, H. Langmaack, and A. Pnueli, editors. Compositionality: The Significant Difference, volume 1536 of LNCS. Springer-Verlag, 1997.Google Scholar
  14. [EL87]
    E.A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275–306, 1987.MATHCrossRefMathSciNetGoogle Scholar
  15. [Fis96]
    K. Fisler. A Unified Approachto Hardware Verification Througha Heterogeneous Logic of Design Diagrams. PhD thesis, Computer Science Department, Indiana University, August 1996.Google Scholar
  16. [HHK96]
    R.H. Hardin, Z. Har’el, and R.P. Kurshan. COSPAN. In CAV, volume 1102 of LNCS, 1996.Google Scholar
  17. [Hol97]
    G. Holzmann. The SPIN model checker. IEEE Transactions on Software Engineering, 23(5), May 1997.Google Scholar
  18. [HP94]
    G.J. Holzmann and D. Peled. An improvement in formal verification. In FORTE, 1994.Google Scholar
  19. [KW01]
    J. Klose and H. Wittke. An automata based interpretation of live sequence charts. In TACAS, volume 2031 of LNCS, 2001.Google Scholar
  20. [LL94]
    P.B. Ladkin and S. Leue. What do message sequence charts mean? In Formal Description Techniques, 1994.Google Scholar
  21. [LP85]
    O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specifications. In POPL, 1985.Google Scholar
  22. [MP87]
    Z. Manna and A. Pnueli. Specification and verification of concurrent programs by forall-automata. In POPL, 1987.Google Scholar
  23. [MP00]
    A. Muscholl and D. Peled. Analyzing message sequence charts. In 2nd Workshop on SDL and MSC, 2000.Google Scholar
  24. [MPS98]
    A. Muscholl, D. Peled, and Z. Su. Deciding properties for message sequence charts. In FoSSaCS, 1998.Google Scholar
  25. [NT00]
    K.S. Namjoshi and R.J. Trefler. On the completeness of compositional reasoning. In CAV, volume 1855 of LNCS. Springer-Verlag, 2000.Google Scholar
  26. [PR99]
    M. Plathand M. Ryan. Feature integration using a feature construct. Science of Computer Programming, 41(1), 1999.Google Scholar
  27. [SHE01]
    M.H. Smith, G.J. Holzmann, and K. Etessami. Events and constraints: A graphical editor for capturing logic requirements of programs. In 5th International Symposium on Requirements Engineering, 2001.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Nina Amla
    • 1
  • E. Allen Emerson
    • 2
  • Kedar S. Namjoshi
    • 3
  • Richard J. Trefler
    • 4
  1. 1.Cadence Design SystemsUSA
  2. 2.Department of Computer SciencesUniversity of Texas at AustinUSA
  3. 3.Bell LaboratoriesLucent TechnologiesUSA
  4. 4.School of Computer ScienceUniversity of WaterlooUSA

Personalised recommendations