Formalizing and Verifying UML Activity Diagrams

UML (Unified Modelling Language) is the de facto standard for the development of software models. Static aspects of systems are mainly described with UML class diagrams. However, the behavioral aspects are often designed by UML state machine and activity diagrams. Due to the ambiguous semantics of UML diagrams, formal methods can be used to generate the corresponding formal specifications and then check their properties. In this paper, we opt for functional semantics of UML activity diagrams by means of FoCaLiZe, a proof based formal method. Thus, we generate formal specifications in order to detect eventual inconsistencies of UML activity diagrams using Zenon, the automatic theorem prover of FoCaLiZe. The proposed approach directly supports action constraints, activity partitions and the communication between structural (classes) and dynamic (activity diagrams) aspects.