Declarative modelling languages, such as Dash and Alloy, allow the user to describe the behaviour of a system abstractly and concisely.
Dash provides the user with the syntax and semantics to specify transition systems using control state hierarchy, transition guards and actions on dynamic variables and trigger events. Dash uses Alloy expressions to specify formulas in the initial conditions, invariants, guards, and actions of the model. Dynamic variables and formulas are modelled using Alloy constructs such as sets and relations. Model checking of Dash models is done by translating the model into Alloy and using the Alloy Analyzer to perform symbolic, bounded model checking for finite scopes. The use of sets and relations in a model greatly contributes to the state space explosion problem. Thus, exploring the entire reachable state space of a model in the Alloy Analyzer is rarely possible.

One of the leading strategies to address the state space explosion problem is Counterexample Guided Abstraction and Refinement (CEGAR). In this seminar, we investigate how the CEGAR framework can be used for bounded model checking of Dash models. Our goal in using CEGAR is to explore more of the reachable state space of the original/concrete model and/or perform bounded model checking at higher scopes than possible with the concrete model. We construct an abstract, conservative model that replaces all concrete model variables (sets and relations) with Boolean variables, thereby creating a smaller model to model check.

However, there are many options for how to use the general principles of CEGAR. The main challenges in our approach are choosing the predicates to construct the abstract model, abstracting the guards and actions of transitions, reducing counterexample validation in the concrete model to take less time than concrete model checking by itself, and minimizing the number of refinement loops needed for the CEGAR loop to terminate.

Our key contributions begin by recognizing that the user abstractions of control states and transitions in Dash by themselves partition the state space of the model into equivalence classes. We can utilize this partition directly in constructing a conservative abstraction of the original model, which puts very useful reachability constraints on the abstract model. Next, we present and evaluate different schemes that vary the choice of predicates over the dynamic variables for the initial abstraction, vary how conservatively we abstract the transition guards and actions, and reduce the counterexample validation and refinement process. We compare the different schemes based on how efficient each scheme is in exploring longer traces in the reachable state space, and traces of a model with large scopes for signatures.