Advertisement

Verifying Intuition — ILF Checks DAWN Proofs

  • Thomas Baar
  • Ekkart Kindler
  • Hagen Völzer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1639)

Abstract p ]The DAWN approach allows to model and verify distributed algorithms in an intuitive way. At a first glance, a DAWN proof may appear to be informal. In this paper, we argue that DAWN proofs are formal and can be checked for correctness fully automatically by automated theorem provers. The basic technique are proof rules which generate proof obligations. For the definition of the proof rules we adopt assertions and we introduce conflict formulas for algebraic Petri nets. Experiments show that the generated proof obligations can be automatically checked by theorem provers.

The DAWN approach allows to model and verify distributed algorithms in an intuitive way. At a first glance, a DAWN proof may appear to be informal. In this paper, we argue that DAWN proofs are formal and can be checked for correctness fully automatically by automated theorem provers. The basic technique are proof rules which generate proof obligations. For the definition of the proof rules we adopt assertions and we introduce conflict formulas for algebraic Petri nets. Experiments show that the generated proof obligations can be automatically checked by theorem provers.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    T. Baar, B. Fischer, and D. Fuchs. Integrating Deductional Techniques in a Software Reuse Application. In: Journal of Universal Computer Science 1999.Google Scholar
  2. 2.
    T. Baar, E. Kindler, H. Völzer. Verifying Intuition — ILF checks DAWN proofs. Informatik-Bericht 119, Humboldt-Universität zu Berlin, March 1999.Google Scholar
  3. 3.
    P. Baumgartner and U. Furbach. Protein: A prover with a theory extension interface. In Proc. CADE-12, pp. 769–773. Springer, 1994.Google Scholar
  4. 4.
    E. Best and C. Fernández. Nonsequential Processes, EATCS Monographs on Theoretical Computer Science 13. Springer-Verlag, 1988.Google Scholar
  5. 5.
    K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.Google Scholar
  6. 6.
    P. Cousot. Methods and logics for proving programs. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 841–993. Elsevier, 1990.Google Scholar
  7. 7.
    B. I. Dahn and J. Denzinger. Cooperating theorem provers. In Automated Deduction — A Basis for Applications, Volume 2, pp. 383–416. Kluwer Academic Publishers, 1998.Google Scholar
  8. 8.
    B. I. Dahn, J. Gehne, T. Honigmann, and A. Wolf. Integration of automated and interactive theorem proving in Ilf. In Proc. CADE-14, pp. 55–60. Springer, 1997.Google Scholar
  9. 9.
    J. Desel and E. Kindler. Proving correctness of distributed algorithms using highlevel Petri nets — a case study. In Proc. CSD 1998, pp. 177–186, Fukushima, Japan, Mar. 1998. IEEE Computer Society Press.Google Scholar
  10. 10.
    C. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent developments (system abstract). In CADE-12, pp. 778–782. Springer, 1994.Google Scholar
  11. 11.
    C. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, Oct. 1969.zbMATHCrossRefGoogle Scholar
  12. 12.
    E. Kindler and W. Reisig. Verification of distributed algorithms with algebraic Petri nets. In C. Freksa, M. Jantzen, and R. Valk (eds.), Foundations of Computer Science: Potential — Theory — Cognition, LNCS 1337, pp. 261–270. Springer, 1997.Google Scholar
  13. 13.
    E. Kindler, W. Reisig, H. Völzer, and R. Walter. Petri net based verification of distributed algorithms: An example. Formal Aspects of Comp., 9:409–424, 1997.zbMATHCrossRefGoogle Scholar
  14. 14.
    E. Kindler and H. Völzer. Flexibility in algebraic nets. In J. Desel and M. Silva (eds.), Application and Theory of Petri Nets 1998, 19 th International Conference, LNCS 1420, pp. 345–364. Springer-Verlag, June 1998.CrossRefGoogle Scholar
  15. 15.
    L. Lamport. The temporal logic of actions. SRC Research Report 79, Digital Equipment Corporation, Systems Research Center, Dec. 1991.Google Scholar
  16. 16.
    Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In 10 th Annual Symposium on Principles of Programming Languages. ACM, Jan. 1983.Google Scholar
  17. 17.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems —; Specification. Springer-Verlag, 1992.Google Scholar
  18. 18.
    Z. Manna and A. Pnueli. A temporal proof methodology for reactive systems. In M. Broy (ed.), Program Design Calculi, Springer, pp. 287–323, 1992.Google Scholar
  19. 19.
    W. McCune. OTTER 2.0: Recent developments (system abstract). In Proc. CADE-10, pp. 663–664. Springer, 1990.Google Scholar
  20. 20.
    S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. Prog. Lang. Syst., 4(3):455–495, July 1982.zbMATHCrossRefGoogle Scholar
  21. 21.
    W. Reisig. Elements of Distributed Algorithms—; Modeling and Analysis with Petri Nets. Springer, 1998.Google Scholar
  22. 22.
    W. Reisig, E. Kindler, T. Vesper, H. Völzer, and R. Walter. Distributed algorithms for networks of agents. In W. Reisig and G. Rozenberg (eds.), Lectures on Petri Nets II: Applications, LNCS 1492, pp. 331–385. Springer, 1998.Google Scholar
  23. 23.
    S. Unger. Automatisches Überprüfen von DAWN-Beweisen. Diploma thesis, Humboldt-Universität zu Berlin, April 1999, forthcoming.Google Scholar
  24. 24.
    M. Weber, R. Walter, H. Völzer, T. Vesper, W. Reisig, S. Peuker, E. Kindler, J. Freiheit, and J. Desel. DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen. Informatik-Bericht 88, Humboldt-Universität zu Berlin, Dec. 1997.Google Scholar
  25. 25.
    C. Weidenbach, B. Gaede, and G. Rock. Spass & Flotter, version 0.42. In CADE-13, pp. 141–145. Springer, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Thomas Baar
    • 1
  • Ekkart Kindler
    • 2
  • Hagen Völzer
    • 2
  1. 1.Humboldt-Universität zu BerlinInstitut für MathematikBerlinGermany
  2. 2.Humboldt-Universität zu BerlinInstitut für InformatikBerlinGermany

Personalised recommendations