A classification and comparison of model checking software architecture techniques

Software architecture specifications are used for many different purposes, such as documenting architectural decisions, predicting architectural qualities before the system is implemented, and guiding the design and coding process. In these contexts, assessing the architectural model as early as possible becomes a relevant challenge. Various analysis techniques have been proposed for testing, model checking, and evaluating performance based on architectural models. Among them, model checking is an exhaustive and automatic verification technique, used to verify whether an architectural specification conforms to expected properties. While model checking is being extensively applied to software architectures, little work has been done to comprehensively enumerate and classify these different techniques. The goal of this paper is to investigate the state-of-the-art in model checking software architectures. For this purpose, we first define the main activities in a model checking software architecture process. Then, we define a classification and comparison framework and compare model checking software architecture techniques according to it. (C) 2009 Elsevier Inc. All rights reserved.