A framework for verifying deadlock and nondeterminism in UML activity diagrams based on CSP

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.