|
>Publications>ASE01 |
Henry Muccini
Ph.D. in Computer Science |
|
{ASE2001}
"Automated Check of Architectural Models Consistency using SPIN"
P. Inverardi, H. Muccini and P. Pelliccione.
Proc. Automated Software Engineering conference, ASE2001, November 2001
|
Abstract:
Architectural description techniques are a key element of the development
of large systems. In recent years several formalisms and models have
been introduced to represent the software architectural level of description.
These models represent SA from different viewpoints, handling different
aspects of the system separately and allowing for analysis and validation
of the architectural choices, both behavioral and quantitative. 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 with respect to analysis and validation:
system specification {\em incompleteness} and {\em 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.
|
|
|
Full Paper
|
[ASE
Presentation] | |
|