A formalism for reasoning about UML activity diagrams
Vitus S. W. Lam · Nordic journal of computing · 2007
The major problem of UML activity diagrams is the lack of a rigorous approach for verifying the correctness of a model. In this paper, we examine how activity diagrams defined in UML 2.0 standard are formally analyzed using NuSMV model checker. A model represented as activity diagrams is first transformed into NuSMV input language and then verified that a set of system specifications is satisfied using NuSMV.