Browsing Theses by Supervisor "Day, Nancy"
Now showing items 1-10 of 10
-
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: 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 ...