On the fly model checking of communicating UML state machines

In this paper we present an 'on the fly' model checker for the verification of the dynamic behavior of UML models seen as a set communicating state machines. The logic supported by the tool is an extension of the action based branching time temporal logic mu-actl and has the power of full mu-calculus. Early result on the application of this model checker to a case study have been also reported.