Browsing Theses by Supervisor "Day, Nancy"
Now showing items 1-11 of 11
-
Astra: Evaluating Translations from Alloy to SMT-LIB
(University of Waterloo, 2018-12-21)We present a variety of translation options for converting Alloy to SMT-LIB via Alloy's Kodkod interface. Our translations, which are implemented in a library that we call Astra, are based on converting the set and relational ... -
A Comprehensive Study of Declarative Modelling Languages
(University of Waterloo, 2020-07-14)Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system functionality abstractly and formally. An abstract model is a concise and compact representation of key characteristics ... -
Dash+: Extending Alloy with Replicated Processes for Modelling Transition Systems
(University of Waterloo, 2022-09-27)Modelling systems abstractly shows great promise to uncover bugs early in system development. The formal language Alloy provides the means of writing constraints abstractly but lacks explicit constructs for describing ... -
Dash: Declarative Behavioural Modelling in Alloy
(University of Waterloo, 2019-01-25)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 ... -
Detection of Feature Interactions in Automotive Active Safety Features
(University of Waterloo, 2012-05-02)With the introduction of software into cars, many functions are now realized with reduced cost, weight and energy. The development of these software systems is done in a distributed manner independently by suppliers, ... -
Improvements to Transitive-Closure-based Model Checking in Alloy
(University of Waterloo, 2018-01-19)Model checking, which refers to the verification of temporal properties of a transition system, is a common formal method for verifying models. Transitive-closure-based model checking (TCMC), developed by Vakili et al., ... -
Linking Alloy with SMT-based Finite Model Finding
(University of Waterloo, 2021-01-28)Alloy is a well-known declarative language for modelling systems early in the development process. Currently, it uses the Kodkod library as its back-end for finite model finding (finding instances of the model by determining ... -
Mapping Template Semantics to SMV
(University of Waterloo, 2004)Template semantics is a template-based approach to describing the semantics of model-based notations, where a pre-defined template captures the notations' common semantics, and parameters specify the notations' distinct ... -
Prescriptive Semantics For Big-Step Modelling Languages
(University of Waterloo, 2011-02-22)With the popularity of model-driven methodologies and the abundance of modelling languages, a major question for a modeller is: Which language is suitable for modelling a system under study? To answer this question, one ... -
Profiling Alloy Models
(University of Waterloo, 2021-09-03)Modeling of software-intensive systems using formal declarative modeling languages offers a means of managing software complexity through the use of abstraction and early identification of correctness issues by formal ... -
Temporal Logic Model Checking as Automated Theorem Proving
(University of Waterloo, 2016-01-19)Model checking is an automatic technique for the verification of temporal properties of a system. In this technique, a system is represented as a labelled graph and the specification as a temporal logic formula. The core ...