Dash: Declarative Behavioural Modelling in Alloy
| dc.contributor.author | Serna, Jose | |
| dc.date.accessioned | 2019-01-25T17:19:59Z | |
| dc.date.available | 2019-01-25T17:19:59Z | |
| dc.date.issued | 2019-01-25 | |
| dc.date.submitted | 2019-01-15 | |
| 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 |
| dc.identifier.uri | http://hdl.handle.net/10012/14424 | |
| dc.language.iso | en | en |
| dc.pending | false | |
| dc.publisher | University of Waterloo | en |
| dc.subject | Alloy | en |
| dc.subject | Behavioural modelling | en |
| dc.subject | Transition system | en |
| dc.subject | statecharts | en |
| dc.title | Dash: Declarative Behavioural Modelling in Alloy | en |
| dc.type | Master Thesis | en |
| uws-etd.degree | Master of Mathematics | en |
| uws-etd.degree.department | David R. Cheriton School of Computer Science | en |
| uws-etd.degree.discipline | Computer Science | en |
| uws-etd.degree.grantor | University of Waterloo | en |
| uws.contributor.advisor | Day, Nancy | |
| uws.contributor.affiliation1 | Faculty of Mathematics | en |
| uws.peerReviewStatus | Unreviewed | en |
| uws.published.city | Waterloo | en |
| uws.published.country | Canada | en |
| uws.published.province | Ontario | en |
| uws.scholarLevel | Graduate | en |
| uws.typeOfResource | Text | en |