Abstract
This paper introduces a method to combine finite automata, parallel programs and SDL (Specification and Description Language) specifications. We base our approach on M-nets exploiting the rich set of composition operators available in this algebra of high-level Petri nets. In order to be able to combine different modelling techniques, we rely on compatible interfaces. Therefore,
-
-
we extend an existing semantics, namely the M-net semantics for the parallel programming language B(PN)2; and
-
-
we present an M-net semantics for finite automata.
Considering the hybrid modelling of an ARQ (Automatic Repeat re-Quest) protocol, we show how the different formalisms fit together as well as the resulting verification possibilities. As a side-effect we describe on-going development of the PEP tool (Programming Environment based on Petri Nets). As a consequence of our approach we are introducing a hierarchical ‘programming with nets’ method which is currently implemented in the high-level Petri net editor of the tool.
Chapter PDF
Keywords
References
M. Ackermann. Konzeption eines Compilers für eine parallele Programmiersprache mit Prozeduren. Diploma thesis, Universität Hildesheim, 1997.
M. v. d. Beeck, V. Braun, A. Claßen, A. Dannecker, C. Friedrich, D. Koschützki, T. Margaria, F. Schreiber, and B. Steffen. Graphs in METAFrame: The Unifying Power of Polymorphism, In E. Brinksma, editor, Proc. of TACAS'97, Enschede, LNCS 1217, 112–129, Springer, 1997.
E. Best. Partial Order Verification with PEP. In G. Holzmann, D. Peled, and V. Pratt, editors, Proc. of POMIV'96, Princeton, 305–328. Am. Math. Soc, 1996.
E. Best, R. Devillers, and J. G. Hall. The Box Calculus: a New Causal Algebra with Multi-Label Communication. In G. Rozenberg, editor, Advances in Petri Nets 92, LNCS 609, 21–69. Springer, 1992.
E. Best, H. Fleischhack, W. Fraczak, R. P. Hopkins, H. Klaudel, and E. Pelz. An M-Net Semantics of B(PN)2. In J. Desel, editor, Proc. of STRICT, Workshops in Computing, 85–100, Springer, 1995.
E. Best, H. Fleischhack, W. Fraczak, R. P. Hopkins, H. Klaudel, and E. Pelz. A Class of Composable High Level Petri Nets. G. De Michelis and M. Diaz, editors, Proc. of ATPN'95, Torino, LNCS 935, 103–118. Springer, 1995.
E. Best and B. Grahlmann. PEP: Documentation and User Guide. Universität Hildesheim. Available together with the tool via: http://www.informatik.uni-hildesheim.de/~pep.
E. Best and R. P. Hopkins. B(PN)2 — a Basic Petri Net Programming Notation. A. Bode, M. Reeve, and G. Wolf, editors, Proc. of PARLE, LNCS 694, 379–390, Springer, 1993.
CCITT. Specification and Description Language, CCITT Z.100, Geneva, 1992.
E. Clarke, K. McMillan, S. Campos, and V. Hartonas-Garmhausen. Symbolic Model Checking. In R. Alur and T. A. Henzinger, editors, Proc. of CAV'96, New Brunswick, LNCS 1102, 419–422, Springer, 1996.
J. Esparza, S. Römer, and W. Vogler. An Improvement of McMillan's Unfolding Algorithm. In T. Margaria and B. Steffen, editors, Proc. of TACAS'96, Passau, LNCS 1055, 87–106, Springer, 1996.
J. Esparza. Model Checking Using Net Unfoldings. In Number 23 in Science of Computer Programming, 151–195, Elsevier, 1994.
H. Fleischhack and B. Grahlmann. A Petri Net Semantics for B(PN)2 with Procedures. Proc. of PDSE'97, 15–27, Boston, IEEE Comp. Soc. Press, 1997.
H. Fleischhack and B. Grahlmann. A Compositional Petri Net Semantics for SDL, Technical report, HIB 18/97, Universität Hildesheim, 1997.
H. Fleischhack and B. Grahlmann. Towards Compositional Verification of SDL Systems. Proc. of 31st HICSS — Software Technology Track, 404–414, IEEE Computer Society Press. 1998.
B. Grahlmann, M. Moeller, and U. Anhalt. A New Interface for the PEP Tool — Parallel Finite Automata. Proc. of 2. Workshop Algorithmen und Werkzeuge für Petrinetze, AIS 22, 21–26. FB Informatik Universität Oldenburg, 1995.
B. Grahlmann. The Reference Component of PEP. In E. Brinksma, editor, Proc. of TACAS'97, Enschede, LNCS 1217, 65–80, Springer, 1997.
B. Grahlmann. The PEP Tool. In O. Grumberg, editor, Proc. of CAV'97, Haifa, LNCS 1254, 440–443, Springer, 1997.
B. Graves. Computing Reachability Properties Hidden in Finite Net Unfoldings. Proc. of FST&TCS'97. LNCS, Springer. 1997.
G. Holzmann and D. Peled. The State of SPIN. In R. Alur and T. A. Henzinger, editors, Proc. of CAV'96, New Brunswick, LNCS 1102, 385–389. Springer, 1996.
J. E. Hopcraft and J. D. Ullmann. Introduction to Automata Theory, and Languages, and Computation. Addison Wesley, 1994.
B. W. Kernighan and D. M. Ritchie. The C Programming Language Prentice Hall, 1988.
S. Melzer and J. Esparza. Checking System Properties via Integer Programming. In H. R. Nielson, editor, Proc. of ESOP'96, LNCS 1058, 250–264, Springer, 1996.
S. Melzer and S. Römer. Synchronisierende Automaten in PEP. Proc. of 3. Workshop Algorithmen und Werkzeuge für Petrinetze, Technical Report 341, 52–59. AIFB Universität Karlsruhe, 1996.
C. Sibertin-Blanc. Cooperative Nets. In R. Valette, editor, Proc. of ATPN'94, LNCS 815, 471–490, Springer, 1994.
P. H. Starke. INA: Integrated Net Analyzer. Handbuch, cf. http://www.informatik.hu-berlin.de/~starke/ina.html.
G. Wimmel. A BDD-based Model Checker for the PEP Tool. Technical Report, University of Newcastle upon Tyne, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grahlmann, B. (1998). Combining finite automata, parallel programs and SDL using Petri nets. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054167
Download citation
DOI: https://doi.org/10.1007/BFb0054167
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive