Distinguishing Environment and System in Coloured Petri Net Models of Reactive Systems

This paper introduces and formally defines the environment-and-system-partitioned property for behavioral models of reactive systems expressed in the formal modeling language coloured Petri net. The purpose of the formalization is to make it possible to automatically validate any CPN model with respect to this property based on structural analysis. A model has the environment-and-system-partitioned property if it is based on a clear division between environment and system. This division is important in many model-driven approaches to software development such as model-based testing and automated code-generation from models. A prototypical tool has been implemented for performing the structural analysis of coloured Petri net models and the principles of this tool is described. The aim of the paper is to make the guidelines and their formalized definitions along with a proof-of-concept for the automatic validation of the structure of models based on structural analysis.