Model Checking UML Activity Diagrams in FDR

The Unified Modeling Language (UML) is the de-facto industrial standard for modeling object-oriented software systems. UML activity diagrams (ADs) can be used for software modeling and they have under gone significant changes with UML 2.0 specification, and no longer been a special kind of diagrams of UML state machines. ADs, however, are lack of formal semantics like other diagrams in UML official specifications and therefore they cannot be performed formal system behavior analysis. Verify if a UML model meets the required properties by model checking has become a key issue. Many attempts have been made to provide formalization for UML state diagrams, but little for ADs. This paper formalize the UML ADs and then employs the Hoarepsilas communicating sequential processes to specify its operational and behavior semantics. The presented formalization makes it possible to reason about the behavior of a UML AD in CSP. A software tool for supporting to transfer an AD into CSPM specification has been implemented. Hence it provides an approach to model checking UML ADs by model-checker FDR. Finally, the formalisms and model checking are explicitly illustrated through a simple but non-trivial example.