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.
Collections
Cite this version of the work
Jose Serna, Nancy A. Day, Shahram Esmaeilsabzali
(2023).
Dash: declarative behavioural modelling in Alloy with control state hierarchy. UWSpace.
http://hdl.handle.net/10012/19628
Other formats