Combining finite automata, parallel programs and SDL using petri nets

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.