| dc.description.abstract | An abstract model is a representation of the fundamental characteristics and properties
of a system, and its purpose is to provide feedback to stakeholders about the correctness
of the system during the early stages of development. This thesis presents Dash, a new
language for the formal specification of abstract behavioural models, which combines the
control-oriented constructs of statecharts with the declarative modelling of Alloy. From
statecharts, Dash inherits a means to specify hierarchy, concurrency, and communication,
three useful aspects to describe the behaviour of reactive systems. From Alloy, Dash uses
the expressiveness of relational logic and set theory to abstractly and declaratively describe
structures, data, and operations.
The purpose of a Dash model is to formally describe a transition system, and for this
reason transitions are first-class constructs of the language. Dash provides features such as
factoring, transition comprehension, and layering, to systematically declare and organise
the transitions of a model.
The integration between statecharts and Alloy is done in Dash at the semantic level.
The semantics of Dash use the notion of big steps and small steps to formally describe
changes in a system, and address the mismatch between declarative and control-oriented
formalisms regarding the frame problem.
This thesis presents several case studies to demonstrate the modelling capabilities and
automated analysis of Dash models. The case studies range from heavily data-oriented
systems to highly hierarchical and concurrent systems. Behaviours can be specified using
a temporal logic and the Alloy Analyzer is used for performing analyses. We extended the
notion of significance axioms and significant scopes to concurrent Dash models, to avoid
spurious instances of a model and ensure that a big enough search space is explored by the
Analyzer to check for interesting behaviours and provide useful feedback about a model. | en |
