Skip to main content
SpringerLink
Log in

A case study in verification based on trace abstractions

  • Conference paper
  • First Online:
Formal Systems Specification

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1169))

Abstract

In [14], we proposed a framework for the automatic verification of reactive systems. Our main tool is a decision procedure, Mona, for Monadic Second-order Logic (M2L) on finite strings. Mona translates a formula in M2L into a finite-state automaton. We show in [14] how traces, i.e. finite executions, and their abstractions can be described behaviorally. These state-less descriptions can be formulated in terms of customized temporal logic operators or idioms.

In the present paper, we give a self-contained, introductory account of our method applied to the RPC-memory specification problem of the 1994 Dagstuhl Seminar on Specification and Refinement of Reactive Systems. The purely behavioral descriptions that we formulate from the informal specifications are formulas that may span 10 pages or more.

Such descriptions are a couple of magnitudes larger than usual temporal logic formulas found in the literature on verification. To securely write these formulas, we use Fido [16] as a reactive system description language. Fido is designed as a high-level symbolic language for expressing regular properties about recursive data structures.

All of our descriptions have been verified automatically by Mona from M2L formulas generated by Fido.

Our work shows that complex behaviors of reactive systems can be formulated and reasoned about without explicit state-based programming. With Fido, we can state temporal properties succinctly while enjoying automated analysis and verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. This volume.

    Google Scholar 

  2. M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.

    Article  Google Scholar 

  3. M. Abadi and L. Lamport. Conjoining specifications. Technical Report Report 118, Digital Equipment Corporation, Systems Research Center, 1993.

    Google Scholar 

  4. M. Broy and L. Lamport. The RPC-Memory Specification Problem. A case study for the Dagstuhl Seminar 9439. This volume.

    Google Scholar 

  5. E.M. Clark, I.A. Browne, and R.P. Kurshan. A unified approach for showing language containment and equivalence between various types of ω-automata. In A. Arnold, editor, CAAP, LNCS 431, pages 103–116, 1990.

    Google Scholar 

  6. R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 15(1):36–72, jan 1993.

    Article  Google Scholar 

  7. E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 16, pages 995–1072. MIT Press/Elsevier, 1990.

    Google Scholar 

  8. U. Engberg, P. Grønning, and L. Lamport. Mechanical verification of concurrent systems with tla. In Computer Aided Verification, CAV '92. Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 663.

    Google Scholar 

  9. U. Engberg. Reasoning in temporal logic of actions. Ph.D. Thesis, 1996.

    Google Scholar 

  10. Z. Har'El and R.P. Kurshan. Software for analytical development of communications protocols. Technical report, AT&T Technical Journal, 1990.

    Google Scholar 

  11. J.G. Henriksen, O.J.L. Jensen, M.E. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A.B. Sandholm. Mona: Monadic second-order logic in practice. In U.H. Engberg, K.G. Larsen, and A. Skou, editors, Procedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 58–73, 1995. BRICS Notes Series NS-95-2.

    Google Scholar 

  12. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

    Google Scholar 

  13. Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification and simulation and refinement. In A Decade of Concurrency, pages 273–346. ACM, Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 803, Proceedings of the REX School/Symposium, Noordwijkerhout, The Netherlands, June 1993.

    Google Scholar 

  14. N. Klarlund, M. Nielsen, and K. Sunesen. Automated logical verification based on trace abstractions. In Proc. Fifteenth ACM Symp. on Princ. of Distributed Computing (PODC). ACM, 1996.

    Google Scholar 

  15. N. Klarlund and F.B. Schneider. Proving nondeterministically specified safety properties using progress measures. Information and Computation, 107(1):151–170, 1993.

    Article  Google Scholar 

  16. N. Klarlund and M.I. Schwartzbach. Logical programming for regular trees. In preparation, 1996.

    Google Scholar 

  17. R. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.

    Google Scholar 

  18. L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, 1983.

    Article  Google Scholar 

  19. L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, 1994.

    Article  Google Scholar 

  20. N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. Sixth Symp. on the Principles of Distributed Computing, pages 137–151. ACM, 1987.

    Google Scholar 

  21. N. Lynch and F. W. Vaandrager. Forward and backward simulations — part I: untimed systems. Technical Report CS-R9313, Centrum voor Wiskunde en Informatica, CWI, Computer Science/Department of Software Technology, 1993.

    Google Scholar 

  22. Z. Manna and et al. STeP: The stanford temporal prover. In Theory and Practice of Software Development (TAPSOFT). Springer-Verlag, 1995. Lecture Notes in Computer Science, Vol. 915.

    Google Scholar 

  23. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.

    Google Scholar 

  24. K. L. McMillan. Symbolic Model Checking. PhD thesis, Carnegie Mellon University, 1993.

    Google Scholar 

  25. A.P. Sistla. On verifying that a concurrent program satisfies a nondeterministic specification. Information Processing Letters, 32(1):17–24, July 1989.

    Article  Google Scholar 

Download references

Author information

Author notes

  1. Nils Klarlund

    Present address: AT&T Research, Room 2C-410, 600 Mountain Ave., 07974, Murray Hill, NJ

Authors and Affiliations

  1. Basic Research in Computer Science, Centre of the Danish National Research Foundation, Department of Computer Science, University of Aarhus, Ny Munkegade, DK-8000, Aarhus C.

    Nils Klarlund, Mogens Nielsen & Kim Sunesen

Authors
  1. Nils Klarlund
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mogens Nielsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim Sunesen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nils Klarlund .

Editor information

Manfred Broy Stephan Merz Katharina Spies

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klarlund, N., Nielsen, M., Sunesen, K. (1996). A case study in verification based on trace abstractions. In: Broy, M., Merz, S., Spies, K. (eds) Formal Systems Specification. Lecture Notes in Computer Science, vol 1169. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024435

Download citation

  • DOI: https://doi.org/10.1007/BFb0024435

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61984-0

  • Online ISBN: 978-3-540-49573-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation