Structured State Space Exploration of Dash+ Models

Model checking is a formal verification technique that plays a crucial role in software engineering in ensuring the correctness of a system. Declarative models are a useful method of expressing the description of a software system during the early stages of development. However, one of the major challenges in model checking of declarative models is the state-space explosion problem. We introduce the idea of structured state-space exploration (S3E), a novel approach to combat state-space explosion in hierarchical transition systems. The motivating idea behind this approach is to utilize the structure of the model found in the user's description, such as the control state hierarchy or guards and actions on the transitions, to derive abstractions that can lead to a reduction in the number of states and/or transitions in the model at the Kripke structure level of description of the model. The proposed methodologies are implemented and evaluated on Dash+ models.