An abstract model is a representation of the fundamental characteristics and propertiesof a system, and its purpose is to provide feedback to stakeholders about the correctnessof the system during the early stages of development. This thesis presents Dash, a newlanguage for the formal specification of abstract behavioural models, which combines thecontrol-oriented constructs of statecharts with the declarative modelling of Alloy. Fromstatecharts, Dash inherits a means to specify hierarchy, concurrency, and communication,three useful aspects to describe the behaviour of reactive systems. From Alloy, Dash usesthe expressiveness of relational logic and set theory to abstractly and declaratively describestructures, data, and operations.The purpose of a Dash model is to formally describe a transition system, and for thisreason transitions are first-class constructs of the language. Dash provides features such asfactoring, transition comprehension, and layering, to systematically declare and organisethe 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 describechanges in a system, and address the mismatch between declarative and control-orientedformalisms regarding the frame problem.This thesis presents several case studies to demonstrate the modelling capabilities andautomated analysis of Dash models. The case studies range from heavily data-orientedsystems to highly hierarchical and concurrent systems. Behaviours can be specified usinga temporal logic and the Alloy Analyzer is used for performing analyses. We extended thenotion of significance axioms and significant scopes to concurrent Dash models, to avoidspurious instances of a model and ensure that a big enough search space is explored by theAnalyzer to check for interesting behaviours and provide useful feedback about a model.
PDF
download
878987797
028-85220240
