In: Steffen, B.: Lecture Notes in Computer Science, Vol. 1384: Proceedings of TACAS'98 (Tools and Algorithms for the Construction and Analysis of Systems), pages 102-117. Springer-Verlag, March 1998. Available at http://www.informatik.uni-hildesheim.de/~pep.
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 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.
Keywords: B(PN)2; Finite automata; Hybrid system design; M-nets; Parallel programs; PEP; Petri nets; SDL; Verification.