×

Petri net based verification of distributed algorithms: An example. (English) Zbl 0889.68071


MSC:

68W15 Distributed algorithms
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

PEP; UNITY
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.: An axiomatization of Lamport’s temporal logic of actions. SRC Research Report 65, Digital Equipment Corporation, Systems Research Center, October 1990.
[2] Apt, K. R. and Olderog, E.-R.:Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer-Verlag, 1991. · Zbl 0733.68053
[3] Best, E., Devillers, R. and Hall, F. G.: The box calculus: A new causal algebra with multi-label communication. In G. Rozenberg, editor,Advances in Petri nets 1992, volume 609 ofLNCS, pages 21-69. Springer-Verlag, 1992.
[4] Best, E. and Grahlmann, B.: ProjectPEP. http://www.informatik.unihildesheim.de/ pep/HomePage.html.
[5] Bougé, L.: Modularité et symétrie pour les systèmes répartis; application au langage CSP. Rapport de Recherche 87-2, Lab. d’Informatique de L’Ecole Normale Superieure, Paris, 1987.
[6] Cuéllar, J., Barnard, D. and Huber, M.: A solution relying on the model checking of boolean transition systems. In M. Broy, S. Merz and K. Spies, editors, Formal Systems Specification, The RPC-Memory Specification Case Study, LNCS 1169.
[7] Chang, E. J. H.: Echo algorithms: Depth parallel operations on general graphs.IEEE Transactions on Software Engineering, SE-8(4):391-401, 1982. · Zbl 05341587 · doi:10.1109/TSE.1982.235573
[8] Chandy, K. M. and Misra, J.:Parallel Program Design: A Foundation. Addison-Wesley, 1988. · Zbl 0717.68034
[9] Desel, J., Neuendorf, K.-P. and Radola, M.-D.: Proving nonreachability by moduloinvariants.Theoretical Computer Science, 153:49-64, 1996. · Zbl 0872.68131 · doi:10.1016/0304-3975(95)00117-4
[10] Dijkstra, E. W. and Scholten, C. S.: Diffusing computations.Information Processing Letters, 1981.
[11] Grahlmann, B. and Best, E.: PEP ? more than a Petri net tool. In T. Margaria and B. Steffen, editors,Tools and Algorithms for the Construction and Analysis of Systems,TACAS, LNCS 1055, pp. 397-401. Springer-Verlag, March 1996.
[12] Gallager, R. G. A., Humblet, P. and Spira, M.: A distributed algorithm for minimumweight spanning trees.ACM Transactions on Programming Languages and Systems, 5(1):66-77, 1983. · Zbl 0498.68040 · doi:10.1145/357195.357200
[13] Jensen, K.:Coloured Petri Nets, volume 1 ofEATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1992.
[14] Kindler, E. and Walter, R.: Message passing mutex. In Jörg Desel, editor,Structures in Concurrency Theory, Workshops in Computing, pages 205-219. Berlin, Springer-Verlag, May 1995.
[15] Lamport, L.: The temporal logic of actions. SRC Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991.
[16] Lynch, N. and Tuttle, M.: An introduction to input/output automata.CWI-Quarterly, 3(2):219-246, 1989. · Zbl 0677.68067
[17] Lynch, N. A.:Distributed Algorihms. Morgan Kaufmann, 1996.
[18] Reisig, W.: Petri net models of distributed algorithms. In Jan van Leeuwen, editor,Computer Science Today: Recent Trends and Developments, LNCS 1000, pp. 441-454. Springer-Verlag, 1995.
[19] Reisig, W.: Modelling and verification of distributed algorithms. In Ugo Montanari and Vladimiro Sassone, editors,CONCUR’96: Concurrency Theory, LNCS 1119, pp. 579-595. Springer-Verlag, 1996.
[20] Raynal, M. and Helary, J.-M.:Synchronization and Control of Distributed Systems and Programs. Series in parallel computing. Wiley, 1990. · Zbl 0751.68026
[21] Stomp, F. A. and de Roever, W. P.: A principle for sequential phased reasoning about distributed algorithms.Formal Aspects of Computing, 6:716-737, 1994. · Zbl 0829.68066
[22] Segall, A.: Distributed network protocols.IEEE Transactions on Information Theory, IT29-1:23-35, 1983. · Zbl 0531.94026 · doi:10.1109/TIT.1983.1056620
[23] Shavit, N. and Francez, N.: A new approach to detection of locally indicative stability. In L. Kott, editor,Proc. of th 13th ICALP, LNCS 226, pp. 344-358. Springer-Verlag, 1986. · Zbl 0594.68029
[24] Tel, G.:Introduction to Distributed Algorithms. Cambridge University Press, 1994. · Zbl 0826.68056
[25] Walter, R., Völzer, H., Vesper, T., Reisig, W., Kindler, E., Freiheit, J. and Desel, J.: Memorandum: Petrinetzmodelle zur Verifikation Verteilter Algorithmen. Informatik-Bericht 67, Humboldt-Universität zu Berlin, July 1996.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.