English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Deadlock and nondeterminism may become increasingly hard to detect inconcurrent and distributed systems. UML activity diagrams are flowcharts thatmodel sequential and concurrent behavior. Although the UML community widelyadopts such diagrams, there is no standard approach to verify the presence ofdeadlock and nondeterministic behavior in activity diagrams. Nondeterminism isusually neglected in the literature even though it may be considered a veryrelevant property. This work proposes a framework for the automaticverification of deadlock and nondeterminism in UML activity diagrams. Itintroduces a compositional CSP semantics for activity diagrams that is used toautomatically generate CSP specifications from UML models. These specificationsare the input for the automatic verification of deadlock and nondeterministicbehavior using the FDR refinement checker. We propose a plugin for the Astahmodeling environment that mechanizes the translation process, and that callsFDR in the background to perform the verification of properties. The tool keepsthe traceability between a diagram and its CSP specification. It parses the FDRresults to highlight the diagram paths that lead to a deadlock or anondeterministic behavior. This framework adds verification capabilities to theUML modeling tool and keeps the formal semantics transparent to the users.Therefore, the user does not need to understand or manipulate formal notationsduring modeling. We present the results of a case study that applies theproposed framework for the verification of models in the domain of cloudcomputing. We discuss future applications due to the potential of our approach.

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