|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
University of Kashan (IRAN)
|
|---|---|
| Method: |
LOTOS
CSP |
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
FDR |
| 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: https://doi.org/10.1016/j.csi.2023.103739 |
| Contact: | Seyed Morteza Babamir Department of Computer Engineering Faculty of Electrical and Computer Engineering University of Kashan Kashan IRAN Email: babamir@kashanu.ac.ir |
| Further remarks: | This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page