Paper Info
Title
From Formal Test Objectives to TTCN-3 for Verifying ETCS Complex Software Control Systems.
Abstract
The design of a practical but accurate software methodology to guarantee systems correctness and safety is still a big challenge. Where test coverage is dissatisfying, formal analysis grants much higher potential to discover errors or safety vulnerabilities during the design phase of a system. However, formal verification methods often require a strong technical background that limits their usage. In this paper, we present a framework based on testing and verification to ensure the correctness and safety of complex distributed software systems. As a result of the application of our methodology we obtain a more reliable system, in terms of functionality, safety and robustness and a reduction of the time necessary for verification. In order to show the applicability of our solution we applied it on a real industrial case study, that is the European Train Control System (ETCS) [14]. We specify the system using the SDL language [24], and we use a test generation tool to generate abstract test cases in TTCN-3. Based on these standardized tests, we verify using model-checking, some critical properties of the system, in particular these regarding safety requirements. We analyse a real train accident and we demonstrate how the accident could have been avoided if the ETCS system was used.
Year
DOI
Venue
2019
10.1007/978-3-030-52991-8_8
ICSOFT
DocType
Volume
Citations 
Conference
1250
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Rabéa Ameur-Boulifa100.34
Ana R. Cavalli267176.11
Stephane Maag322927.21