In: 97: Proceedings of the Workshop on Petri Nets in System Engineering (PNSE'97), Hamburg, September 25-26, 1997 / Farwer, B.; Moldt, D.; Stehr, M.-O.: Report FBI-HH-B-205, pages 32-43. Universität Hamburg, September 1997.
Abstract: In this paper, we consider state space analysis of Hierarchical 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 this 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 exploiting the hierarchical structure of the models.
Keywords: state space based approaches; efficient model checking; tools; coloured Petri nets; validation; simulation.