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.
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Hooman, Jozef; Kugler, Hillel; Ober, Iulian; Votintseva, Anjelika; Yushtein, Yuri: Supporting UML-based development of embedded systems by formal techniques (2008)
- Xie, Fei; Levin, Vladimir; Browne, James C.: ObjectCheck: A model checking tool for executable object-oriented software system designs (2002)