Reducing software architecture models complexity: A slicing and abstraction approach

Software architectures (SA) represents a critical design level for software systems. Architectural choices need to be analyzed and verified to achieve a better software quality while reducing the time and cost of production. Model-checking is one of the most promising verification techniques, however its use for very large systems is not always possible due to the state explosion problem. In this paper we propose an approach that slices and abstracts the SA of a system in order to reduce the model complexity without compromising the verification validity. This approach exploits the characteristics of the SA model and the structure of the property of interest. It is applied to an industrial telecommunication system of the Selex Communications company.