Abstract
We present a state space exploration method for on-the-fly verification. The method is aimed at systems for which it is possible to define a measure of progress based on the states of the system. The measure of progress makes it possible to delete certain states on-the-fly during state space generation, since these states can never be reached again. This in turn reduces the memory used for state space storage during the task of verification. Examples of progress measures are sequence numbers in communication protocols and time in certain models with time. We illustrate the application of the method on a number of Coloured Petri Net models, and give a first evaluation of its practicality by means of an implementation based on the Design/CPN state space tool. Our experiments show significant reductions in both space and time used during state space exploration. The method is not specific to Coloured Petri Nets but applicable to a wide range of modelling languages.
| Original language | English |
|---|---|
| Title of host publication | Lecture Notes in Computer Science |
| Number of pages | 15 |
| Volume | 2031 |
| Publisher | Springer |
| Publication date | 2001 |
| Edition | Lecture Notes in Computer Science 2031 |
| Pages | 450-464 |
| ISBN (Print) | 978-3-540-41865-8 |
| Publication status | Published - 2001 |
| Event | Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001) - Genova, Italy Duration: 2 Apr 2001 → 6 Apr 2001 Conference number: 7 |
Conference
| Conference | Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001) |
|---|---|
| Number | 7 |
| Country/Territory | Italy |
| City | Genova |
| Period | 02/04/2001 → 06/04/2001 |