Institut Mines-Télécom / Télécom ParisTech
Institut Mines-Télécom / Télécom SudParis
CADP (Construction and Analysis of Distributed Processes)
The development, verification, and testing of complex software systems
(e.g., embedded systems, control systems, etc.) involve high challenges
due to the complexity of the implementation and the time required
for testing and verifying. Many efforts have been put into the
processes of software validation and in particular in the testing of
these systems from the verification of formal specifications. However,
although languages and formal transformation have been proposed for
that purpose, very few works have been devoted to the verification of
models from the testing phases.
The framework proposed here, based on formal methods, aims at automating the development and verification processes, and particularly at verifying software systems from the standardized definition of their test objectives. The main components of the framework are: a transformation that converts IF test-objectives to MCL formulas in such a way that automatic and exhaustive verification of safety properties will be possible on the system under study; a toolchain for automating test generation, complemented with formal verification features.
The methodology was applied on a real industrial case study, namely the ETCS (European Train Control System). Over the past century, Europe's railways have been developed within national boundaries, resulting in a variety of different signaling and train control systems, which hampers cross-border traffic. In the scope of increasing their interoperability, the European Union has decided to adopt a standard, the ETCS. Some components of this standard were formalized in FIACRE (and subsequently translated into pNets), and based on standardized test objectives, some critical properties of the system were verified using CADP.
The proposed framework enables the generation of logical properties
from test objectives with the goal of verifying properties on complex
distributed systems. The expected result consists in a more reliable
system, in terms of functionality, safety and robustness, and a
reduction of the time necessary for verification.
Rabéa Ameur-Boulifa, Anna Cavalli, and Stéphane Maag.
"Verifying Complex Software Control Systems from Test Objectives:
Application to the ETCS System".
Proceedings of the 14th International Conference on Software
Technologies ICSOFT'2019 (Prague, Czech Republic), pp. 397-406,
SciTePress, July 2019.
Available on-line at: http://www.scitepress.org/DigitalLibrary/Link.aspx?doi=10.5220/0007918203970406
or from the CADP Web site in PDF or PostScript
Laboratoire System-On-Chip, TELECOM ParisTech
Les Templiers, 450, route des Chappes, F-06410 Biot
Tel: +33 (0)4 93 00 84 01
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|