Derivation of formal representations from process-based specification and implementation models
Steven Vercauteren, Diederik Verkest, Gjalt de Jong, Binshan Lin · 1997
In this paper we present a formal framework to ver-ify timing properties of embedded systems. We propose a process calculus as an intermediate model to map be-tween language-level constructs of process-based specifica-tion and implementation models, and Petri net operations. We present an elegant translation scheme to generate Petri nets starting from the intermediate process expressions. The approach has been applied to verify the freedom of deadlock in a QAM modem design, with promising results. 1.