Database of Research Tools Developed Using CADP

UML Model Checker

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

Last modified: Tue Mar 19 17:42:40 2024.

Back to the CADP research tools page