DASH: Declarative Modelling with Control State Hierarchy (Preliminary Version)

Abstract

We present a new language, called DASH, for describing formal behavioural models. DASH combines common modelling constructs to describe abstractly both data and control in an integrated manner. DASH uses the Alloy language for describing data and its operations declaratively, and adds syntax for labelled control state hierarchy common in Statecharts descriptions of transition systems. In addition, DASH accommodates multiple factoring paradigms for modelling (control states, events, and conditions) and includes syntactic sugar (e.g., transition comprehension, transition templates) to write models that are concise and easy to understand. We describe the formal semantics of DASH, which carefully mix the usual semantic understanding of control state hierarchy with the declarative perspective, for creating abstract models early in system development. We implement these semantics in a translator from DASH to Alloy taking advantage of Alloy language features. We demonstrate DASH, our tool, and model checking analysis in the Alloy Analyzer using several case studies. The key novel insight of our work is in combining seamlessly common data and control modelling paradigms in a way that will be intuitive for those used to either paradigm, and enabling automatic analysis of the integrated model.