|
|
|
| Untersuchte Arbeit: Seite: 57, Zeilen: (16), 17-30 |
Quelle: Schäfer et al 2001 Seite(n): 1-2, Zeilen: 1:30-33-2:1-10.18-21 |
|---|---|
| 2.4.2 HUGO Model Checker
HUGO is a prototype tool designed to automatically verify whether the interactions expressed by a collaboration diagram can indeed be realized by a set of state machines. Technically, this is achieved by compiling state machines into a PROMELA model, and collaborations into sets of BÜchi automata 2 (” never claim”). The model checker SPIN is then called to verify the model against the automata. The idea to analyze UML state machines and other variants of Statecharts using model checking has been suggested before [Kwo00,LMM99,LP99, MLS97, MLSH99], but HUGO is based on dynamic computation of Statechart behavior rather than a pre-determined, static calculation of possible state transitions in response to input events. HUGO has the advantage of being more modular, more flexible, and easier to adapt to variants of Statechart semantics, including possible changes to the semantics of UML state machines. Besides model checking, HUGO also supports animation and the generation of Java code from UML state machine models, based on the same structure of implementation. HUGO provides us also the correctness of the generated code with respect to the properties verified from the PROMELA model. (see figure 2.11) 2 A Büchi automata is the extension of a finite state machine to infinite inputs. It accepts an infinite input sequence, iff there exists a run of the automaton (in case of a deterministic automaton, there is exactly one possible run) which has infinitely many states in the set of final states. It is named after the Swiss mathematician Julius Richard Büchi. Finite state machine (FSM) is a model of behavior composed of a finite number of states, transitions between those states, and actions. [Kwo00] G. Kwon. Rewrite rules and operational semantics for model checking uml statecharts. In : A. Evans, S. Kent and B. Selic, editors, Proc. 3nd Int. Conf. UML, Lect. Notes Comp. Sci. 1939, pages 528–440, 2000. [LMM99] D. Latella, I. Majzik, and M. Massink. Automatic verification of a behavioural subset of uml statechart diagrams using the spin model-checker. In Formal Aspects Comp. 11, pages 637–664, 1999. [LP99] J. Lilius and I. P. Paltor. Formalising uml state machines for model checking. In : R. B. France and B. Rumpe, editors, Proc. 2nd Int. Conf. UML, Lect. Notes Comp. Sci. 1723, pages 430–445, 1999. [MLS97] E. Mikk, Y. Lakhnech, and M. Siegel. Hierarchical automata as model for statecharts. In : R. K. Shyamasundar and K. Ueda, editors, Proc. 3nd Asian Computing Science Conf., Lect. Notes Comp. Sci. 1345, pages 181–196, 1997. [MLSH99] E. Mikk, Y. Lakhnech, M. Siegel, and G.J. Holzmann. Implementing statecharts in promela/spin. In Proc. Wsh. Industrial-Strength Formal Specification Techniques, 1999. |
[page 1]
In this paper we describe HUGO, a prototype tool designed to automatically verify whether the interactions expressed by a collaboration diagram can indeed be realized by a set of state machines. Technically, this is achieved by compiling state machines into a PROMELA [1] model, and collaborations into sets of Büchi [page 2] automata (“never claims”). The model checker SPIN is then called upon to verify the model against the automata. The idea to analyze UML state machines and other variants of Statecharts using model checking has been suggested before [2,3,4,5,6], although we are not aware of other tools that verify state machines against collaboration diagrams. In contrast to most other encodings of Statecharts, ours is based on a dynamic computation of Statechart behavior rather than a pre-determined, static calculation of possible state transitions in response to input events. Our approach has the advantage of being more modular, more flexible, and easier to adapt to variants of Statechart semantics, including possible changes to the semantics of UML state machines. [...] Besides model checking, HUGO also supports animation and the generation of Java code from UML state machine models, based on the same structure of implementation. Our aim is to ensure the correctness of the generated code with respect to the properties verified from the PROMELA model. [1] Holzmann, G. J., The SPIN Model Checker, IEEE Trans. Softw. Eng. 23 (1997), pp. 279–295. [2] Kwon, G., Rewrite Rules and Operational Semantics for Model Checking UML Statecharts, in: A. Evans, S. Kent and B. Selic, editors, Proc. 3nd Int. Conf. UML, Lect. Notes Comp. Sci. 1939 (2000), pp. 528–540. [3] Latella, D., I. Majzik and M. Massink, Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-Checker, Formal Aspects Comp. 11 (1999), pp. 637–664. [4] Lilius, J. and I. P. Paltor, Formalising UML State Machines for Model Checking, in: R. B. France and B. Rumpe, editors, Proc. 2nd Int. Conf. UML, Lect. Notes Comp. Sci. 1723 (1999), pp. 430–445. [5] Mikk, E., Y. Lakhnech and M. Siegel, Hierarchical Automata as Model for Statecharts, in: R. K. Shyamasundar and K. Ueda, editors, Proc. 3rd Asian Computing Science Conf., Lect. Notes Comp. Sci. 1345 (1997), pp. 181–196. [6] Mikk, E., Y. Lakhnech, M. Siegel and G. J. Holzmann, Implementing Statecharts in Promela/SPIN, in: Proc. IEEE Wsh. Industrial-Strength Formal Specification Techniques (1999). |
Although identical - including references - nothing has been marked as a citation. the original source is not given here. |
|