Formal Verification and Validation of Industrial Railway Train Spacing System

The Faculty of Informatics is pleased to announce a seminar given by Andrei Tcshaltsev

DATE: Tuesday, February 21st, 2012
PLACE: USI Università della Svizzera italiana, room SI-006, Informatics building (Via G. Buffi 13)
TIME: 13.30

ABSTRACT:
In this talk I will describe an industrial application of formal methods for the verification and validation of "Logica di Sicurezza" (LDS), the safety logic of a railways ERTMS Level 2 system developed by Ansaldo-STS for Italian Railway and Transportation Systems. LDS is a generic control software that is instantiated on a railways network configuration. We developed a methodology for the verification and validation of a critical subset of LDS deployed on typical realistic railways network configurations. To show feasibility, effectiveness and scalability, we have experimented with several state of the art symbolic software model checking techniques and tools on different network configurations. From the experiments, we have successfully identified an effective strategy for the verification and validation of our case study. Moreover, the results of experiments show that formal verification and validation is feasible and effective, and also scales reasonably well with the size of the configuration. Given the results, Ansaldo-STS is currently integrating the methodology in its internal Development and Verification & Validation Flow.

BIO:
In 2004, I've got PhD of Computer Science in the Formal Methods group of the Department  at Manchester University, UK. The research topic was on the development of practical means for specifying the semantics of programming languages and the validation of code generation and static analysis.
In 2004-2011, I worked in the Embedded Systems Research Unit of the Foundation of Bruno Kessler (FBK), Italy. The research areas I took part in are model checking, embedded software and hardware verification, scheduling, realizability and synthesis of reactive systems. During these years I took part in the development of several scientific tools, of which the most well known one is NuSMV Model Checker. During the last 2-3 years I worked in projects  focused on verification of real-life industrial safety-critical controlling systems. Here the goal was to obtain the practical results for particular set of large programs. My talk will be about the last such project focused on verification of  software signaling and automation systems for Ansaldo, a technology company operating in Italian Railway and Transportation Systems.

HOST: Prof. Natasha Sharygina