%0 Conference Paper %1 grahlmann1998a %A Grahlmann, Bernd %B Proceedings of TACAS'98 (Tools and Algorithms for the Construction and Analysis of Systems) %D 1998 %E Steffen, Bernhard %I Springer-Verlag %K PEP, B(PN)$^2$, M-nets, design, programs, Finite Parallel Hybrid Petri automata, SDL, Verification. system nets, %P 102--117 %T Combining Finite Automata, Parallel Programs and SDL Using Petri Nets. %V 1384 %X 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, itemize 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. itemize Considering the hybrid modelling of an ARQ (Automatic Repeat reQuest) 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.

@inproceedings{grahlmann1998a, 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, \begin{itemize} \item we extend an existing semantics, namely the M-net semantics for the parallel programming language B(PN)$^2$; and \item we present an M-net semantics for finite automata. \end{itemize} Considering the hybrid modelling of an ARQ (Automatic Repeat reQuest) 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. }, added-at = {2006-03-09T08:15:35.000+0100}, author = {Grahlmann, Bernd}, biburl = {https://www.bibsonomy.org/bibtex/2ab348f0bd8c37508030b9cec26e72b2e/snowball}, booktitle = {{Proceedings of TACAS'98 (Tools and Algorithms for the Construction and Analysis of Systems)}}, editor = {Steffen, Bernhard}, interhash = {31b67364f7a0ce5e3dae68aa54b5673a}, intrahash = {ab348f0bd8c37508030b9cec26e72b2e}, keywords = {PEP, B(PN)$^2$, M-nets, design, programs, Finite Parallel Hybrid Petri automata, SDL, Verification. system nets,}, month = {March}, pages = {{102--117}}, publisher = {{Springer-Verlag}}, series = {{Lecture Notes in Computer Science}}, timestamp = {2006-03-09T08:15:35.000+0100}, title = {{Combining Finite Automata, Parallel Programs and SDL Using Petri Nets.}}, volume = {{1384}}, year = {{1998}} }