SAFETY PROPERTIES IN PETRI NET MODULES

Article type: Research Article

Authors: Padberg, Julia

Affiliations: Institute for Software Technology and Theoretical Computer Science, Technical University Berlin, Germany

Abstract: This paper introduces safety properties in the temporal logic sense (as defined in (Manna and Pnueli, 1995)) to Petri net modules. Petri net modules (Padberg, 2001, Padberg, 2002) have been achieved by a transfer of algebraic specification modules to Petri nets. They consist of three nets; the interface nets import and export, and the body of the module. The import net states the prerequisites the modules assumes. The body net represents the internal functionality. The export net gives an abstraction of the body that can be used by the environment. The interfaces IMP and EXP are related to the body BOD via morphisms. These modules conform with the basic concepts of components and component-based systems of Continuous Software Engineering (CSE) (Weber, 1999). We make precise what it means that a Petri net module has specific safety properties. We differentiate between explicit and implicit properties. Explicit safety properties are stated additionally to the export net. Implicit are those properties that hold in the export net without being stated explicitly. The main advantage of our approach are module operations to compose larger modules from basic ones. We can show that the composition of modules preserves safety properties: Given two modules with implicit or explicit safety properties then the composition of these modules is again a module with implicit or explicit safety properties.

Keywords: Module, Petri nets, Safety property

Journal: Journal of Integrated Design & Process Science, vol. 8, no. 4, pp. 65-78, 2004