Dash is a new modelling language for the specification and verification of system behaviour. This site provides documentation about the language, several case studies, and an online editor for using Dash.

Dash provides syntactic constructs to specify and factor transitions. Transitions can be factored by states as is done in state charts, or can also be grouped by events and/or conditions; this make Dash a flexible language that can acomodate different paradigms of modelling. Additionally, Dash provides transition comprehension, a feature that allows the description of a group of transitions with a single statement (e.g., transitions from every state to an error state). Furthermore, addons in Dash make declarations of transitions modular. Components of transitions can be describbed in different parts of a model and then, at analysis time, they are merged together to form the complete definition of a transition. For example, it is possible to define an action LogError that can later be added to all transitions that go to an error state.

Behavioural properties can be specified in Computation Tree Logic (CTL), a temporal logic that allows the verification of a desired property in all possible executions of a model.


Dash members

Former members