Synthesis and Verification of Models using Satisfiability Modulo Theories

Abstract

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.