Synthesis and Verification of Models using Satisfiability Modulo Theories
Model-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.
URI for this recordhttp://hdl.handle.net/1974/27585
Request an alternative formatIf you require this document in an alternate, accessible format, please contact the Queen's Adaptive Technology Centre
The following license files are associated with this item:
Showing items related by title, author, creator and subject.
Sequential Model-Based A- and V-Optimal Design of Experiments for Building Fundamental Models of Pharmaceutical Production Processes Shahmohammadi, Ali; McAuley, Kimberley B. (Elsevier BV, 2019-07-02)Sequential model-based A- and V-optimal experimental designs are known to be effective for maximizing the information content of data, leading to reliable parameter estimates and model predictions. A- and V-optimal designs ...
Transferability of Regional Permafrost Disturbance Susceptibility Modelling Using Generalized Linear and Generalized Additive Models Rudy, Ashley C.A; Lamoureux, Scott F.; Treitz, Paul; Van Ewijk, Karin Y. (2016-06-16)To effectively assess and mitigate risk of permafrost disturbance, disturbance-p rone areas can be predicted through the application of susceptibility models. In this study we developed regional susceptibility models ...
The Use of Medical Scans from Patients as a Tool for 3D modelling, and Printing of Anatomical Models for Surgical Education Ienceanu, Vlad (2019-04-30)There is an ongoing concern associated with realistic anatomical teaching due to the shortage in available cadavers and inaccurate synthetic models. With plaster models having reduced accuracy due to the process of creation, ...