Verifying Complex Software Control Systems from Test Objectives

Organisation:	Institut Mines-Télécom / Télécom ParisTech Institut Mines-Télécom / Télécom SudParis Université Paris-Saclay
Method:	FIACRE pNets
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Railways.
Period:	2019
Size:	4 pNets
Description:	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.
Conclusions:	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.
Publications:	[AmeurBoulifa-Cavalli-Maag-19] 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
Contact:	Rabéa Ameur-Boulifa Laboratoire System-On-Chip, TELECOM ParisTech Institut EURECOM Les Templiers, 450, route des Chappes, F-06410 Biot FRANCE Tel: +33 (0)4 93 00 84 01 Email: Rabea.Ameur-Boulifa@telecom-paristech.fr
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