Engineering Support for UML Activities by Automated Model-Checking
RISE 2007 Workshop, (2007)Abstract
In our approach for the engineering of reactive services, we specify systems as collaborations by means of UML 2.0 activities. In automated and correctness-preserving steps, the collaborative models are transformed into executable code. The semantics of the activities are defined using temporal logic. This formal fundament can be utilized to prove that the collaborations fulfill certain general well-formedness properties which can be verified by the model checker TLC. This is quite relevant since communication delays in the interactions between the participants realizing a collaboration aggravate the design of correct collaborative behavior. The well-known state space explosion problem of model checkers is mitigated by using special external state machines which define the interface behavior of sub-activities. The generation of the formal input for TLC from the activities is completely automated, so that the engineers working on the activities do not need to be experts in temporal logic and model checking. In this paper, we describe the utilization of TLC to detect and correct design errors by means of an example.