Verifying complex software control systems from test objectives: Application to the ETCS system

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Ensuring the correctness of complex distributed software systems is a challenging task, the issue of building frameworks for developing such safe and correct systems still remains a difficult issue. Where test coverage is dissatisfying, formal analysis grants much higher potential to discover bugs during the development phase. This paper presents a framework for formal verification of complex systems based on standardized test objectives. The framework integrates a transformation of test objectives into formal properties that are verified on the system by model checking. The overall proposed approach for formal verification is evaluated by the application to the standard European Train Control System (ETCS). Some critical safety properties have been proved on the model, ensuring that the model is correct and reliable.

Original languageEnglish
Title of host publicationICSOFT 2019 - Proceedings of the 14th International Conference on Software Technologies
EditorsMarten van Sinderen, Leszek Maciaszek, Leszek Maciaszek
PublisherSciTePress
Pages397-406
Number of pages10
ISBN (Electronic)9789897583797
DOIs
Publication statusPublished - 1 Jan 2019
Externally publishedYes
Event14th International Conference on Software Technologies, ICSOFT 2019 - Prague, Czech Republic
Duration: 26 Jul 201928 Jul 2019

Publication series

NameICSOFT 2019 - Proceedings of the 14th International Conference on Software Technologies

Conference

Conference14th International Conference on Software Technologies, ICSOFT 2019
Country/TerritoryCzech Republic
CityPrague
Period26/07/1928/07/19

Keywords

  • Formal verification
  • Model checking
  • Safety
  • Software control systems

Fingerprint

Dive into the research topics of 'Verifying complex software control systems from test objectives: Application to the ETCS system'. Together they form a unique fingerprint.

Cite this