Browsing Mathematics (Faculty of) by Author "Day, Nancy A."
Now showing items 1-13 of 13
-
ALDB: Debugging Alloy Models of Behavioural Requirements
Dureja, Aman; Keerthi, Aditya; Liang, Andrew; Zhang, Paul; Day, Nancy A. (IEEE, 2020-08)Declarative modelling languages, such as Alloy, are becoming popular for describing behavioural requirements very early in system development because automated analysis of these models provides valuable feedback. Typically, ... -
Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB
Abbassi, Ali; Day, Nancy A.; Rayside, Derek (2019-06-13)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 Comparison of the Declarative Modelling Languages B, Dash, and TLA+
Abbassi, Ali; Bandali, Amin; Day, Nancy; Serna, Jose (IEEE, 2019-08)Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system func- tionality abstractly and concisely. We compare two well-used formal declarative modelling languages, B and TLA+, ... -
Dash+: Extending Alloy with Hierarchical States and Replicated Processes for Modelling Transition Systems
Hossain, Tamjid; Day, Nancy A. (IEEE, 2021-09)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: A New Language for Declarative Behavioural Requirements with Control State Hierarchy
Serna, Jose; Day, Nancy A.; Farheen, Sabria (IEEE, 2017-09-04)We present DASH, a new language for describing formal behavioural models of requirements. DASH combines the ability to write abstract, declarative transitions (as in Z or Alloy) with a labelled control state hierarchy (as ... -
DASH: Declarative Modelling with Control State Hierarchy (Preliminary Version)
Serna, Jose; Day, Nancy A.; Esmaeilsabzali, Shahram (University of Waterloo, 2018)We present a new language, called DASH, for describing formal behavioural models. DASH combines common modelling constructs to describe abstractly both data and control in an integrated manner. DASH uses the Alloy language ... -
Extracting Counterexamples from Transitive-Closure-Based Model Checking
Kember, Mitchell; Tran, Lynn; Gao, George; Day, Nancy (IEEE, 2019)We address the problem of how to extract counterexamples for the transitive-closure-based model checking (TCMC) technique. TCMC is a representation of the CTLFC (CTL with fairness constraints) model checking problem in ... -
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Vakili, Amirhossein; Day, Nancy A. (Springer, 2016)The problem of finite model finding, finding a satisfying model for a set of first-order logic formulas for a finite scope, is an important step in many verification techniques. In MACE-style solvers, the problem is mapped ... -
Morse: Reducing the Feature Interaction Explosion Problem Using Subject Matter Knowledge as Abstract Requirements
Millet, Laure; Day, Nancy; Joyce, Jeffrey J. (IEEE, 2018-08)The feature interaction problem appears in many different kinds of complex systems, especially systems whose elements are created or maintained by separate entities - for example, a modern automobile that incorporates ... -
Representing Behavioural Models with Rich Control Structures in SMT-LIB
Day, Nancy A.; Vakili, Amirhossein (University of Waterloo, 2015-09-01)We motivate and present a proposal for how to represent extended finite state machine behavioural models with rich hierarchical states and compositional control structures (e.g., the Statecharts family) in SMT-LIB. Our ... -
Representing hierarchical state machine models in SMT-LIB
Day, Nancy A.; Vakili, Amirhossein (ACM, 2016-05)We motivate and present a proposal for how to represent the syntax of behavioural models written in extended finite-state machine languages with hierarchical states (e.g., the Statecharts family) in SMT-LIB. By including ... -
Static Profiling of Alloy Models
Eid, Elias; Day, Nancy A. (IEEE, 2022-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 ... -
Which classes of structures are both pseudo-elementary and definable by an infinitary sentence?
Boney, Will; Csima, Barbara F.; Day, Nancy A.; Harrison-Trainor, Matthew (2019-03-21)When classes of structures are not first-order definable, we might still try to find a nice description. There are two common ways for doing this. One is to expand the language, leading to notions of pseudo-elementary ...