Dash: declarative behavioural modelling in Alloy with control state hierarchy

Abstract

We present Dash, an extension to the Alloy language to model dynamic behaviour using the labelled control state hierarchy of Statecharts. From Statecharts, Dash borrows the concepts to specify hierarchy, concurrency, and communication for describing behaviour in a compositional manner. From Alloy, Dash uses the expressiveness of relational logic and set theory to abstractly and declaratively describe structures, data, and operations. We justify our semantic design decisions for Dash, which carefully mix the usual semantic understanding of control state hierarchy with the declarative perspective. We describe and implement the semantics of a Dash model by translating it to Alloy, taking advantage of Alloy language features. We evaluate our Dash translation and perform model checking analysis, enabled by our translation, in the Alloy Analyzer using several case studies. Dash provides modellers with a language that seamlessly combines the semantics of control-modelling paradigms with Alloy’s existing strengths in modelling data and operations abstractly.