Logic in Railway Verification

Relatore:  Monika Seisenberger - Swansea University, Swansea (Wales)
  venerdì 29 maggio 2020 alle ore 16.00 Online via Zoom
Mathematical methods always played an important role in the verification of Railway control systems.
In this talk we present two different approaches, the first for discrete systems, the second for hybrid systems. Both were used in our collaboration with Industry.
We start with traditional solid state Railway interlockings, often specified using a graphical language called Ladder Logic. We give a semantics for this language
and show how to get from aladder logic specification to a satisfiability problem. This process has been automated, and several existing Interlocking case studies,
provided by our Industrial partner Siemens Rail Automation, have been verified using automated theorem proving tools.
We further applied our own SAT solver, which we extracted from a formal constructive proof of the completeness of the Davis-Putnam-Logemann-Loveland (DPLL) proof
system. The extracted SAT solver is a verified algorithm, which either yields a model or a DPLL refutation of a given clause set [1].
In the second part, we present our modelling of the European Rail Traffic Management System ERTMS, a state-of-the-art train control system, which aims at improving
the performance/capacity of rail traffic systems, without compromising their safety.
It generalizes from traditional interlockings to a system that includes on-board equipment and communication between trains and interlockings via radio block processors. Whilst
the correctness of discrete interlocking systems is well-researched, it is challenging to verify ERTMS based systems for safety properties such as collision freedom due to the
involvement of continuous data. The modelling and verification is done in Real-Time Maude, a tool that allows for both simulation and verification of real-time and hybrid
systems [2].
 
[1] U. Berger, A. Lawrence, F. Nordvall Forsberg, M. Seisenberger, Extracting Verified Decision Procedures: DPLL and Resolution, Logical Methods in Computer Science, 2015.
[2] U. Berger, P. James, A. Lawrence, M. Roggenbach, M. Seisenberger, Verification of the European Rail Traffic Management System in Real-Time Maude,
Science of Computer Programming, JSP 2018.

The seminar will be held online via Zoom:   https://univr.zoom.us/j/96504680574

Contact Person: P. Schuster

Referente

Referente esterno
Data pubblicazione
22 maggio 2020

Offerta formativa

Condividi