Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle

In this paper we describe the use of a model-checking based tool, Charmy, in the Marconi Selenia software development environment. The goal of the project is to model and analyze the software architecture of a software system currently under development. We define and formally check its overall architecture. By zooming into relevant sub-systems we are able to identify a set of incorrect behaviors. We use an iterative process, where both the architectural sub-systems models and the properties to be checked can be defined, checked and revised several times. The results of the experience allow an evaluation of the effort to use the analysis framework in the considered industrial software development environment and an assessment of the efficacy and the role of the architectural analysis in the software development process. The main relevance of this experience is in the effort to smoothly integrate the use of model-checking techniques in a standard software life-cycle, in particular concerning the discovery and definition of architectural properties.