ObjectCheck

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. \parThis paper presents ObjectCheck, a new tool that supports an approach to model checking executable object-oriented software system designs modeled in xUML.