Symbolic methods for the verification of software models

Abstract

One of the major challenges in modern software engineering is dealing with the increasing complexity of software systems. The new paradigm of model-driven engineering (MDE) promises to handle this complexity using the abstraction power of software models based on languages such as the Unified Modeling Language (UML). The objective of MDE is to generate executable code from a set of diagrams with little or no intervention of a developer. These diagrams are referred to as model of the system to be implemented. Usually multi-view models are employed, where each diagram shows a different view on the system, altogether providing a holistic representation. This shift from code-centric development to MDE requires a modeling language based on a solid formal semantics, which is considered one of the major current challenges in MDE research and in future improvements of the UML. Further, with this high valorization of software models, also stronger requirements on their consistency come along since errors introduced on the model level can result in faulty code. The models are central to the evolution of a software system and therefore undergo continuous and often parallel modifications that can introduce inconsistencies. However, necessary consistency management tasks are often too cumbersome to be performed manually due to the size of the models. Hence, automated methods are required. In this work we formalize a modeling language based on the UML. Our language contains two views: the state machine diagram and the sequence diagram. We then identify three problems that can occur in models based on this language. The Sequence Diagram Merging Problem deals with merging two modified versions of a sequence diagram in a way that keeps them consistent with the set of state machines they are related to. The State Machine Reachability Problem asks whether a combination of states in a set of state machines can be reached from some global state by sending and receiving messages between the state machines. The Sequence Diagram Model Checking Problem asks whether a sequence diagram is consistent with the set of state machines it instantiates. For each problem, we propose an encoding to the satisfiability problem of propositional logic (SAT) in order to solve it with an off-the-shelf SAT solver and we determine its computational complexity. We evaluate our approaches based on a set of handcrafted models and on grammar-based whitebox fuzzing, for which we develop a random model generator. The results of our experiments show that we can solve instances of these problems of reasonable size on standard hardware with state-of-the-art SAT solvers.