Dash+: Extending Alloy with Replicated Processes for Modelling Transition Systems

Abstract

Modelling systems abstractly shows great promise to uncover bugs early in system development. The formal language Alloy provides the means of writing constraints abstractly but lacks explicit constructs for describing transition systems. Extensions to Alloy, such as Electrum, DynAlloy, and Dash, provide such constructs. However, still missing are language constructs to describe easily multiple processes with the same behavior (replicated processes) running in parallel as is found in languages such as PlusCal and Promela.

We propose extensions to Dash for replicated processes. The result is Dash+: an Alloy language extension for describing transition systems that include both concurrent and hierarchical states and replicated concurrent processes. The processes can communicate via buffers or exchange information through variables and events. The key contributions of our novel approach are:

1) Replicated and non-replicated components can be nested arbitrarily at any level in the state hierarchy

2) Replicated components can exchange information directly without resorting to global variables as is the case in PlusCal and Promela

3) A modeller can abstractly model the topology of the processes (ring, list, etc.) through constraints on the set indexing the processes

4) Buffers can be used to facilitate communication between replicated components

Dash+ stays consistent with the semantics of Dash and uses the notion of big steps and small steps to describe changes in the system. The semantics are implemented in a translation to Alloy in a way that accommodates the following model checking options: traces-based model checking, transitive closure-based model checking (TCMC), and Electrum.

Our implementation is fully integrated into the Alloy Analyzer. This thesis presents case studies to demonstrate the features of Dash+ in modelling systems with concurrent processes and the benefits that Dash+ offers over existing languages. We check for properties in each of the models in the case studies to demonstrate how different model checking options can be used.