Show simple item record

dc.contributor.authorKahani, Nafisehen
dc.description.abstractModel-driven development (MDD) advocates using models as the primary software development artifacts in place of source code. Automatic synthesis and verification of models are essential to simplify the process of creation and design of high-quality models. Despite its importance, support for synthesis and verification of models remains less than ideal, and it is still the case that no existing MDD tool or technique supports automatic synthesis of models based on the system properties, or handles the verification of models directly, without leveraging program verification tools. The key idea in this thesis is the use of satisfiability modulo theories (SMT) solvers to boost the synthesis and verification capabilities of existing MDD tools. The scope of this work is twofold. First, we propose a synthesis approach using SMT that takes as input a structural model of a system and its desired system properties, and automatically synthesizes executable state machines for its components. To this end, it first generates a synthesis formula for each component consistent with the system properties, and then performs a state space exploration of each component based on its synthesis formula. The result of the state space exploration is saved in a labeled transition system (LTS). Finally, we transform the LTSs into UML-RT (UML for real-time) state machines and integrate them with the original structural models. Unlike any other method, our approach synthesizes detailed actions for the transitions of the synthesized state machines. With action code, synthesized state machines can be executed and tested. Second, we propose a bounded verification approach for hierarchical state machines, which is the main formalism for the description of behavior in many MDD tools. Our approach takes as input the behavior of a system, a depth bound, and the system properties (as invariants), and then automatically verifies models of systems in a four-phase process: (1) It first generates all possible execution paths of the model to the specified bound; (2) it encodes each of the execution paths as SMT formulas; (3) it instruments the SMT formulas with the negation of given invariants; and (4) finally, it uses SMT solvers to check the satisfiability of the instrumented formula.en
dc.relation.ispartofseriesCanadian thesesen
dc.rightsAttribution 3.0 United Statesen
dc.rightsQueen's University's Thesis/Dissertation Non-Exclusive License for Deposit to QSpace and Library and Archives Canadaen
dc.rightsProQuest PhD and Master's Theses International Dissemination Agreementen
dc.rightsIntellectual Property Guidelines at Queen's Universityen
dc.rightsCopying and Preserving Your Thesisen
dc.rightsThis publication is made available by the authority of the copyright owner solely for the purpose of private study and research and may not be copied or reproduced except as permitted by the copyright laws without written authority from the copyright owner.en
dc.subjectSynthesis of Modelsen
dc.subjectVerification of Modelsen
dc.subjectSatisfiability Modulo Theories (SMT Solvers)en
dc.subjectModel Transformationen
dc.subjectState Machinesen
dc.subjectModel-Driven Development (MDD)en
dc.subjectModel-Driven Engineering (MDE)en
dc.subjectReal-Time Embedded (RTE) Systemsen
dc.subjectUML-RT (UML for real-time)en
dc.titleSynthesis and Verification of Models using Satisfiability Modulo Theoriesen
dc.contributor.supervisorCordy, James Ren
dc.contributor.departmentComputingen's University at Kingstonen

Files in this item


This item appears in the following Collection(s)

Show simple item record

Attribution 3.0 United States
Except where otherwise noted, this item's license is described as Attribution 3.0 United States