Analyzing temporal properties of abstract models

Abstract

Models are created and changed throughout the development process of software systems. The cost of repairing the errors that are due to mistakes in models is very high. In this research, we address this problem by developing model checking techniques that can be applied to abstract models that guide designers throughout the evolution of models and systems. Abstract models are declarative, expressed as a set of constraints, and this declarative aspect is the main challenge in model checking them. Our main idea for solving this problem is to express the model checking problem as a constraint solving problem. This approach enables designers to use current state-of-the-art constraint solvers for analysis. We have implemented this idea for Alloy models and we are further extending it for automatic model repairing. To achieve scalability, we have developed BDD-based methods for analysis of declarative models and we are studying model checking methods that are based on satisfiability modulo theories. We plan to extend these methods to infinite state space models.