Transformational implementation of PAISLey specifications using Petri nets

The paper presents a method for the specification and transformational implementation of embedded control systems. The method is based on an extension to Petri nets. The modelling power of the proposed nets is shown by comparison with the functional specification language PAISLey. Extended Petri nets provide a framework for building an executable model of a specification (prototype), automated transformation of the model structure, simulation and validation of the model behaviour, and automated code generation for the validated structure. The method is illustrated using a laboratory process-control system as a working example