Automated Check of Architectural Models Consistency using Spin

In recent years the necessity to handle different aspects of the system separately has introduced the need to represent SA from different viewpoints. In particular, behavioral views are recognized to be one of the most attractive feature in the SA description and in practical contexts, state diagrams and scenarios are the most used tools to model this view. Although very expressive this approach has two drawbacks: system specification incompleteness and view consistency. Our work can be put in this context with the aim to manage incompleteness and to check views conformance: we suppose to have state diagrams and scenarios models representing the system dynamics at the architectural level; they can be incomplete and we want to prove that they describe, from different viewpoints, the same system behavior. To reach this goal, we are using the SPIN model checker and we are implementing a tool to manage the translation of architectural models in Promela and LTL.