Advertisement

Rules for abstraction

  • Stephan Merz
Session I
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)

Abstract

Abstraction techniques for the verification of reactive systems promise to provide a theoretical basis for the integration of automatic and interactive proof techniques. In this paper, we give an account of homomorphic abstraction by studying a series of proof rules in Lamport's Temporal Logic of Actions. We believe that the main advantage of a logical formalization of abstraction is that it points towards more refined abstraction techniques. Specifically, we demonstrate two novel techniques that appear helpful in the verification of liveness properties over abstract models.

Keywords

Model Check Temporal Logic Proof Obligation Liveness Property Transition Formula 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 81(2):253–284, May 1991.CrossRefGoogle Scholar
  2. 2.
    Martin Abadi and Stephan Merz. On TLA as a logic. In Manfred Broy, editor, Deductive Program Design, NATO ASI series F, pages 235–272. Springer-Verlag, Berlin, 1996.Google Scholar
  3. 3.
    S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification: 8th International Conference, volume 1102 of Lecture Notes in Computer Science, pages 323–335. Springer-Verlag, 1996.Google Scholar
  4. 4.
    Nikolaj Bjørner, Anca Browne, Edward Chang, Michael Colón, Arjun Kapur, Zohar Manna, Henny B. Sipma, and Tomás E. Uribe. STeP: deductive-algorithmic verification of reactive and real-time systems. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification: 8th International Conference, volume 1102 of Lecture Notes in Computer Science, pages 415–418. Springer-Verlag, 1996.Google Scholar
  5. 5.
    Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, September 1994. A preliminary version appeared in POPL 1992.CrossRefGoogle Scholar
  6. 6.
    Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977. ACM Press.Google Scholar
  7. 7.
    Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems: Abstractions preserving VCTL, ECTL and CTL. In Ernst-Rüdiger Olderog, editor, Programming Concepts, Methods, and Calculi (PROCOMET '94), pages 561–581, Amsterdam, 1994. IFIP Transactions, North Holland/Elsevier.Google Scholar
  8. 8.
    J. Dingel and T. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In Computer-Aided Verification, volume 939 of Lecture Notes in Computer Science, Berlin, 1995. Springer-Verlag.Google Scholar
  9. 9.
    Susanne Graf and Hassan Saidi. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Computer Aided Verification: 9th International Conference, volume 1254 of Lecture Notes in Computer Science, pages 72–83. Springer-Verlag, 1997.Google Scholar
  10. 10.
    Klaus Havelund and Natarajan Shankar. Experiments in theorem proving and model checking for protocol verification. In Marie-Claude Gaudel and Jim Woodcock, editors, Formal Methods Europe, pages 662–681, Berlin, March 1996. Springer-Verlag.Google Scholar
  11. 11.
    Hermann Hellwagner. Scalable readers/writers synchronization on shared-memory machines. Technical report, Siemens AG, ZFE ST SN 2, 1993.Google Scholar
  12. 12.
    Robert P. Kurshan. Analysis of discrete event coordination. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Proceedings REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 414–454. Springer-Verlag, May 1989.Google Scholar
  13. 13.
    Leslie Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 657–668, Paris, September 1983. IFIP, North-Holland.Google Scholar
  14. 14.
    Leslie Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.CrossRefGoogle Scholar
  15. 15.
    Leslie Lamport and Lawrence C. Paulson. Should your specification language be typed? Research Report 147, Digital Equipment Corporation, Systems Research Center, Palo Alto, California, May 1997.Google Scholar
  16. 16.
    Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, and Saddek Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:11–44, 1995. A preliminary version appeared as Spectre technical report RTC40, Grenoble, France, 1993.CrossRefGoogle Scholar
  17. 17.
    Stephan Merz. Isabelle/TLA. Available on the WWW at URL http://www4. informatik.tu-muenchen.de/-merz/isabelle/, 1997.Google Scholar
  18. 18.
    Olaf Müller and Tobias Nipkow. Combining model checking and deduction for I/O-automata. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, 1995.Google Scholar
  19. 19.
    Ulrich Nitsche and Pierre Wolper. Relative liveness and behavior abstraction. In Principles of Distributed Computing. ACM Press, 1997. to appear.Google Scholar
  20. 20.
    Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.CrossRefGoogle Scholar
  21. 21.
    Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Heidelberg, 1994.Google Scholar
  22. 22.
    Joseph Sifakis. Property preserving homomorphisms of transition systems. In Edmund M. Clarke and Dexter Kozen, editors, 4th Workshop on Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 458–473. Springer-Verlag, June 1983.Google Scholar
  23. 23.
    Bernhard Steifen, Kim G. Larsen, and Carsten Weise. A constraint oriented proof methodology based on modal transition systems. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 17–40. Springer-Verlag, 1995.Google Scholar
  24. 24.
    Wolfgang Thomas. Automata on infinite objects. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 133–194. Elsevier, Amsterdam, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Stephan Merz
    • 1
  1. 1.Institut für InformatikUniversität MünchenGermany

Personalised recommendations