zbMATH — the first resource for mathematics

ObjectCheck: A model checking tool for executable object-oriented software system designs. (English) Zbl 1059.68560
Kutsche, Ralf-Detlef (ed.) et al., Fundamental approaches to software engineering. 5th international conference, FASE 2002. Held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43353-8). Lect. Notes Comput. Sci. 2306, 331-335 (2002).
Summary: Specifying software system designs with executable object-oriented modeling languages such as XUML, an executable dialect of UML, opens the possibility of verifying these system designs by model checking. However, state-of-the-art model checkers are not directly applicable to executable object-oriented software system designs due to the semantic and syntactic gaps between executable object-oriented modeling languages and input languages of these model checkers and also due to the large state spaces of these system designs.
This paper presents ObjectCheck, a new tool that supports an approach to model checking executable object-oriented software system designs modeled in xUML.
For the entire collection see [Zbl 0989.00047].
68N99 Theory of software
Full Text: Link