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
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
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.
- Shahram Esmaeilsabzali
- Sabria Farheen