University of Molise (ITALY)
University of Pisa (ITALY)
CADP (Construction and Analysis of Distributed Processes)
ProM (Process Mining Workbench)
up to 434,073 states and 444,071 transitions
Usually, formal verification is applied to abstract models of a
system, which might differ from the real implementation written in
some programming language. To bridge this gap between the
implementation and the model used for verification, the authors
suggest to retrieve the formal model from concrete execution traces.
Concretely, the authors proceed in three steps:
For each of four scenarios, 2000 LTSs were extracted, and for each of two additional scenarios, 10,000 LTSs were extracted. Then, all nine mu-calculus formulae were checked using CADP, counting, for each property, the number of LTSs were the property was not valid. This allowed to distinguish between correct and incorrect scenarios.
The proposed combination of process mining and model checking was
found a promising approach to bridge the gap between formal
verification on abstract models and a concrete implementation.
Fabio Martinelli, Francesco Mercaldo, Vittoria Nardone, Albina Orlando,
Antonella Santone, and Gigliola Vaglin.
"Safety Critical Systems Formal Verification using Execution Traces".
Proceedings of the 27th IEEE International Conference on Enabling
Technologies: Infrastructure for Collaborative Enterprises (WETICE
2018), Paris, France, pages 247-250, IEEE, June 2018.
Available on-line at: http://doi.org/10.1109/WETICE.2018.00054
or from the CADP Web site in PDF or PostScript
Istituto di Informatica e Telematica - IIT
Area della Ricerca CNR di Pisa
Via. G. Moruzzi 1
56124 Pisa, Italy
Tel: +39 (0)50 315 3425
Fax: +39 (0)50 315 2593
E-mail: fabio.martinelli at iit.cnr.it
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|