Wednesday, January 15, 2020, 10:30 am, GOODWIN HALL Conference Room 524
Supervisor: James Cordy
Internal Examiner: Juergen Dingel
External Internal Examiner: Thomas Dean, ECE
External Examiner: Daniel Amyot, University of Ottawa
Head's Representative: Joshua Dunfield
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 is essential to simplifying the process of creation and design of high-quality models. Automation can also help to facilitate the wider use of models in the development of safety-critical systems, and to enable and stimulate follow-up work on model quality assurance activities such as analysis, model-based testing, and simulation. 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 practical 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. In contrast with previous work, our approach does not require scenario analysis or interaction with expert users. Instead, it takes as input system properties specified as quantifier-free first-order logic formulas that are relatively easy to express. Unlike any other method, our approach also synthesizes detailed actions for the transitions of the generated state machines. In this work we apply our approach in practice, and develop an automated model synthesis tool called AutoModel. We assess the applicability, performance, and scalability of our approach using several different use cases extracted from the literature.
Second, we propose a bounded verification approach for hierarchical state machines, which is the main formalism for the description of behavior in many current modeling tools. Our approach takes as input the behavior of a system, a depth bound, and the system properties (as invariants), and automatically verifies the model of the system. Similarly to bounded verification tools that use SMT solvers for programs, our method does not suffer from the state-space explosion that plagues model checking techniques that use binary decision diagrams. In practice, the majority of errors in real models can be found using verification to a reasonable bound. We have developed a verification tool, called vUMLRT, which embodies our approach and supports the verification of UML-RT (UML for real-time embedded systems) models. We assess the applicability, performance, and scalability of our tool using several case studies extracted from the literature.