In: W. van der Aalst, J.-M. Colom, F. Kordon, G. Kotsis and D. Moldt (Eds.): Petri Net Approaches for Modelling and Validation, Lincom Studies in Computer Science 01, pages 1-16. Lincom Europa, Munich, 2003, 2003.
Abstract: In tis paper, we consider state space analysis of Coloured Petri Nets. It is well-known that almost all dynamic properties of the considered system can be verified when the state space is finite. However, state space analysis is more than just formulating a set of formal requirements and invoking a corresponding set of queries. State space analysis is also applicable during the design and debugging of a system. An approach towards this is to allow the user to analyse the behaviour of systems by drawing and generating selected parts of the state space. The contribution of his paper is to present a tool in which formal verification, partial state spaces, and analysis by means of graphical feedback and simulation are integrated entities. The focus of the paper is twofold: the support for graphical feedback and the way it has been integrated with simulation, and the underlying algorithms and data-structures supporting computation and storage of state spaces which exploi the hierarchical structure of the models.
Keywords: State Space Based Approaches; Efficient Model Checking; Tools; Coloured Petri Nets; Verification and Simulation; Validation.