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.
Niu, Yi (2013-02-01)Clustered failure time data often arise in biomedical and clinical studies where potential correlation among survival times is induced in a cluster. In this thesis, we develop a class of marginal models for right censored ...
Development and assessment of a temperature model and habitat suitability models for spawning Micropterus dolomieu and Micropterus salmoides Sneep, Aaron (2018-04)Micropterus dolomieu (Smallmouth bass) and Micropterus salmoides (Largemouth bass) are two of the most popular recreational fishing species in North America. A lot of effort is put into the management of these species, ...
THE FLEXIBLE CADAVER KNEE MODEL AS A TRAINING MODEL FOR THE DEVELOPMENT OF BASIC ARTHROSCOPIC SKILLS Scribbans, Trisha Dawn (2012-04-26)Goal: Develop an effective high-fidelity model for the purpose of training orthopaedic surgeons. Objectives: This study had two objectives; I) the development of a flexible cadaver model for training orthopaedic surgery ...