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

TL;DR

This paper introduces an automated framework that translates UML activity diagrams into CSP specifications to verify deadlock and nondeterminism, integrating with modeling tools and FDR for formal analysis.

Contribution

It presents a novel compositional CSP semantics for UML activity diagrams and a plugin that automates verification within the Astah environment.

Findings

Successfully verified deadlock and nondeterminism in cloud computing models.

Automated translation from UML to CSP enhances verification efficiency.

Traceability between diagrams and CSP specifications is maintained.

Abstract

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.