A state space tool for concurrent system models expressed in C
Antti Valmari · 2015
This publication introduces a state space exploration tool that is based on representing the model under verification as a piece of C++ code that obeys certain conventions. This approach facilitates experimenting with many kinds of modelling ideas. On the other hand, the use of stubborn sets and symmetries requires that either the modeller or a preprocessor tool analyses the model at a syntactic level and expresses stubborn set obligation rules and the symmetry mapping as suitable C++ functions. The tool supports the detection of illegal deadlocks, safety errors, and may progress errors. It also partially supports the detection of must progress errors.