Database of Case Studies Achieved Using CADP

Verification and Validation of UML Statecharts using Process Algebra

Organisation: University of Kashan (IRAN)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Object-oriented Design.

Period: 2023

Size: n/a

Description: UML is widely used to model systems through diagrams, focusing on understanding models thanks to its visual syntax. However, UML does not deal with the inconsistencies and ambiguities in models. To fix these shortcomings and increase the accuracy of models, formal methods are used, which also bring the ability of checking some behavioral properties that may not be possible with an informal specification.

This work focuses on behavioral diagrams of UML, in particular the Statechart diagram, which describes serial and concurrent runtime behavior of a system in terms of states. An automatic method to validate UML Statecharts is proposed, based on an automated translation from (complete) Statecharts to LOTOS. This enables to verify four generic correctness properties using CADP (deadlock, livelock, state accessibility, and nondeterminism). A fifth property (divergence) is verified using FDR by translating the LOTOS specifications to CSP. The overall approach is illustrated on two case-studies: the dining philosophers and an automatic teller machine.

Conclusions: The proposed method for the verification of UML Statechart diagrams proceeds by mapping UML Statecharts to LOTOS automatically and using CADP and FDR tools for verification. The experimental results demonstrated that the BCG graph model generated by the proposed method is more efficient in time and memory and in verifying properties not previously addressed in related studies.

Publications: [Doostali-Babamir-Javani-23] Saeed Doostali, Seyed Morteza Babamir, and Mohammad Javani. "Using a Process Algebra Interface for Verification and Validation of UML Statecharts". Computer Standards & Interfaces 86:103739, 2023.
Available on-line at:

Seyed Morteza Babamir
Department of Computer Engineering
Faculty of Electrical and Computer Engineering
University of Kashan

Further remarks: This case-study, amongst others, is described on the CADP Web site:

Last modified: Wed Feb 21 11:43:23 2024.

Back to the CADP case studies page