  Deadlock and nondeterminism may become increasingly hard to detect in
concurrent and distributed systems. UML activity diagrams are flowcharts that
model sequential and concurrent behavior. Although the UML community widely
adopts such diagrams, there is no standard approach to verify the presence of
deadlock and nondeterministic behavior in activity diagrams. Nondeterminism is
usually neglected in the literature even though it may be considered a very
relevant property. This work proposes a framework for the automatic
verification of deadlock and nondeterminism in UML activity diagrams. It
introduces a compositional CSP semantics for activity diagrams that is used to
automatically generate CSP specifications from UML models. These specifications
are the input for the automatic verification of deadlock and nondeterministic
behavior using the FDR refinement checker. We propose a plugin for the Astah
modeling environment that mechanizes the translation process, and that calls
FDR in the background to perform the verification of properties. The tool keeps
the traceability between a diagram and its CSP specification. It parses the FDR
results to highlight the diagram paths that lead to a deadlock or a
nondeterministic behavior. This framework adds verification capabilities to the
UML modeling tool and keeps the formal semantics transparent to the users.
Therefore, the user does not need to understand or manipulate formal notations
during modeling. We present the results of a case study that applies the
proposed framework for the verification of models in the domain of cloud
computing. We discuss future applications due to the potential of our approach.
