In: Microprocessing and Microprogramming, Vol. 32, No. 1-5, pages 617-624. 1991.
Abstract: Presents a methodology for transformational design and implementation of embedded software, which is based on an original extension to Petri nets. Basic notion of the method is executable specification which is susceptible of experimental validation. During the transformation phase the specification is subject to automated transformations that preserve its behavioral functionality, but alter the internal structure and performance, in order to meet the requirements of the runtime environment. Mathematical model which underlies the method consists of Petri net, which represents flow of control, and a data path, which represents data processing aspects of the system being designed. This provides a framework for creating an executable specification, automated transformation of the specification structure, simulated execution, and validation of the specification behavior