Model checking for an executable subset of UML

This paper presents an approach to model checking soft-ware system designs specied in an executable subset of UML, xUML. The approach is enabled by the execution semantics of xUML and is based on automatic transla-tion from xUML to S/R [5], the input language of the COSPAN [5] model checker. Translation algorithms are de ned and described, which cover class models, state models of classes, actions associated with states in state models, execution semantics, etc. The translation at-tempts to reduce the state space of the resulting S/R model that is to be veried by COSPAN. An xUML level logic for specifying properties to be checked is dened. Automated support is provided for translating properties speci ed in the logic to S/R representations and mapping error traces generated by COSPAN to xUML representa-tions. The approach is illustrated by some results from a veri cation study of a simplied robot control system.