|
| 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 |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
ISTI/CNR, Pisa (ITALY)
|
|---|---|
| Functionality: |
Model Checking.
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
ProB |
| Period: |
2023
|
| Description: |
Model-based development is an industrially adopted software engineering
technique that supports the creation of models to represent a system's
behaviour and structure. These models are used to generate code,
documentation, test cases, system simulations, and perform other tasks.
Commercial tools for model-based development are often based on the
Unified Modeling Language (UML) OMG standard, which is considered a
semi-formal method. The semantics of semi-formal methods is informally
described in natural language documents, therefore suffering either
from semantic aspects intentionally left open by the standards or
unintentional ambiguities. As a result, the same semi-formal model
executed on different simulators may behave differently.
The UML Model Checker (UMC) is an open-access tool explicitly oriented to the fast prototyping of systems consisting of interacting state machines. UMC allows the user to design a UML state diagram using a simple textual notation, visualise the corresponding graphical representation, interactively animate the system evolutions, formally verify (using on-the-fly model checking) UCTL properties of the system behaviour. Detailed explanations are given when a property is found not to hold, also in terms of simple UML sequence diagrams. With UMC it is possible to check if/how a given transition is eventually fired, if/when a certain signal is sent, if/when a certain variable is modified, or a certain state reached. Since UMC is essentially a teaching/research-oriented academic tool, its stability and support level were enhanced by exploiting other, more industry-ready, formal tools, such as ProB and CADP. This was achieved by developing translators from (a subset of) the UMC notation to the input language of ProB and to LNT. CADP/LNT were selected because of their theoretical roots in Labelled Transition Systems, which allow reasoning in terms of minimization, bisimulation, and compositional verification. CADP is a rich toolbox that supports a wide set of temporal logic and provides a powerful scripting language to automate verification runs. UMC, together with ProB and CADP, has been recently applied to the 4SECURail case-study (see http://cadp.inria.fr/case-studies/22-c-4securail.html ). |
| Conclusions: |
The results of the 4SECURail project have shown how a "formal methods
diversity" approach can be successfully exploited to gain more
confidence in the correctness of the formalization and analysis, and
to gain access to a rich set of options for analyzing the system.
Even without using advanced formal verification techniques (e.g.,
involving bisimulations and complex temporal logic formulas), many
easy-to-use analyses (e.g., static checks, invariants, deadlocks,
reachabilities) can be be performed without any specific advanced
background. This lightweight use of formal methods is not aimed at full
system verification/validation, but remains a very important aid for
the early detection of ambiguities in the natural language requirements
and of errors in their rigorous specification.
|
| Publications: |
[Belli-Fantechi-Gnesi-et-al-23]
Dimitri Belli, Alessandro Fantechi, Stefania Gnesi, Laura Masullo,
Franco Mazzanti, Lisa Quadrini, Daniele Trentini, and Carlo Vaghi.
"The 4SECURail Case Study on Rigorous Standard Interface
Specifications". Proc. of the 28th International Conference on Formal
Methods for Industrial Critical Systems (FMICS'2023), Antwerp, Belgium,
Lecture Notes in Computer Science vol. 14290, pp. 22-39. Springer
Verlag, September 2023.
Available on-line at: https://doi.org/10.1007/978-3-031-43681-9_2 or from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Franco Mazzanti Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo", CNR Via G. Moruzzi 1 56124 Pisa ITALY Email: franco.mazzanti@isti.cnr.it |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page