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.
supported by DFG: Project ‘Deduktion für Fremdnutzer’ within the’ schwerpunktprogramm Deduktion’
supported by DFG: Projects ‘Petri Net Technology’ and ‘Datenkonsistenzkriterien’
supported by DFG: Project’ Konsensalgorithmen’
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
T. Baar, B. Fischer, and D. Fuchs. Integrating Deductional Techniques in a Software Reuse Application. In: Journal of Universal Computer Science 1999.
T. Baar, E. Kindler, H. Völzer. Verifying Intuition — ILF checks DAWN proofs. Informatik-Bericht 119, Humboldt-Universität zu Berlin, March 1999.
P. Baumgartner and U. Furbach. Protein: A prover with a theory extension interface. In Proc. CADE-12, pp. 769–773. Springer, 1994.
E. Best and C. Fernández. Nonsequential Processes, EATCS Monographs on Theoretical Computer Science 13. Springer-Verlag, 1988.
K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
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.
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.
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.
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.
C. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent developments (system abstract). In CADE-12, pp. 778–782. Springer, 1994.
C. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, Oct. 1969.
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.
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.
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.
L. Lamport. The temporal logic of actions. SRC Research Report 79, Digital Equipment Corporation, Systems Research Center, Dec. 1991.
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.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems —; Specification. Springer-Verlag, 1992.
Z. Manna and A. Pnueli. A temporal proof methodology for reactive systems. In M. Broy (ed.), Program Design Calculi, Springer, pp. 287–323, 1992.
W. McCune. OTTER 2.0: Recent developments (system abstract). In Proc. CADE-10, pp. 663–664. Springer, 1990.
S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. Prog. Lang. Syst., 4(3):455–495, July 1982.
W. Reisig. Elements of Distributed Algorithms—; Modeling and Analysis with Petri Nets. Springer, 1998.
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.
S. Unger. Automatisches Überprüfen von DAWN-Beweisen. Diploma thesis, Humboldt-Universität zu Berlin, April 1999, forthcoming.
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.
C. Weidenbach, B. Gaede, and G. Rock. Spass & Flotter, version 0.42. In CADE-13, pp. 141–145. Springer, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baar, T., Kindler, E., Völzer, H. (1999). Verifying Intuition — ILF Checks DAWN Proofs. In: Donatelli, S., Kleijn, J. (eds) Application and Theory of Petri Nets 1999. ICATPN 1999. Lecture Notes in Computer Science, vol 1639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48745-X_24
Download citation
DOI: https://doi.org/10.1007/3-540-48745-X_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66132-0
Online ISBN: 978-3-540-48745-6
eBook Packages: Springer Book Archive