@INPROCEEDINGS{grahlmann:3/98,
        AUTHOR             = {Bernd Grahlmann},
        EDITOR             = {Bernhard Steffen},
        BOOKTITLE          = {{Proceedings of TACAS'98 (Tools and Algorithms
                               for the Construction and Analysis of Systems)}},
        MONTH              = mar,
        PAGES              = {{102--117}},
        PUBLISHER          = {{Springer-Verlag}},
        SERIES             = {{Lecture Notes in Computer Science}},
        VOLUME             = {{1384}},
        TITLE              = {{Combining Finite Automata, Parallel Programs and
                               SDL Using Petri Nets.}},
        YEAR               = {{1998}},
        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.
                             },
        KEYWORDS           = {B(PN)$^2$, Finite automata, Hybrid system design, M-nets,
                              Parallel programs, PEP, Petri nets, SDL, Verification.}
}