Toni Jussila, J. Dubrovin, I. Porres, T. Latvala, T. Junttila,
"Model Checking Dynamic and Hierarchical UML State Machines"
: Proc. 3rd International Workshop on Model Development, Validation and Verification, Seite(n) 94-110, 10-2006
Original Titel:
Model Checking Dynamic and Hierarchical UML State Machines
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 3rd International Workshop on Model Development, Validation and Verification
Original Kurzfassung:
This paper presents a technique to model check UML specifications
by translating UML models to the model checker SPIN. Our models consist of active
UML classes, whose behavior is defined by hierarchical state machines. The
intended application is to find errors in protocols communicating using asynchronous
message passing. Compared to previous efforts using a similar approach,
our novel points are the following. First, we consider a subset of UML
that in our opinion is expressive enough for protocol models but allows a simpler
translation to SPIN than existing work. Preliminary analysis of simple industrial
models support our conclusions on the expressivity of our UML subset. Second,
we present a powerful action language that is still amenable to automatic analysis.
The action language is used to specify the effects of transitions, which may include
dynamic creation of new objects. Finally, we discuss an even simpler SPIN
translation for flattened UML state machines and compare it to the translation
that supports hierarchy.
Forschungs-