Aalst, Willibrordus Martinus Pancratius van der3, Colom, José-Manuel4, Moldt, Daniel7, Kordon, Fabrice5, Kotsis, Gabriela6
1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 AU IT - Operations, AU IT, Central Administration, Aarhus University3 Eindhoven University of Technology4 Centre Polytechnique Supérieur de l'Université de Saragosse5 Université P. & M. Curie6 Univ. Linz7 Universität Hamburg Stadt8 AU IT - Operations, AU IT, Central Administration, Aarhus University
In this 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.
Lincom Studies in Computer Science: Lscs 01: Petri Net Approaches for Modelling and Validation, 2003, Issue 1, p. 1-16
State Space Based Approaches; Efficient Model Checking; Tools; Coloured Petri Nets; Verification and Simulation; Validation