Programme
Tuesday 28th June
12.00 Registration and Coffee
13.00 Welcome from RATP and the Programme Chairs
Session Chair: Alexander Romanovsky
13.10 Keynote 1: Robin Bloomfield (Adelard LLP & City University, UK)
The risk assessment of ERTMS-based railway systems from a cyber perspective:
methodology and lessons learned
14.10 Coffee break
Session: Security. Chair: Ralf Pinger
14.40 Joeri de Ruiter, Richard J Thomas & Tom Chothia (University of Birmingham, UK)
Formal Security Analysis of ERTMS train to Trackside Protocols
15.20 Po-Chi Huang & Birgit Milius (Technische Universität Braunschweig, Germany)
Operational Security –
A Coming Evolution of Railway Operational Procedures under the IT security Threat
16.00 Florent Pépin & Maria Grazia Vigliotti (RSSB, UK)
Risk Assessment of the 3Des in the ERTMS
16.40 Close of Day 1
17.30 Conference reception – Café Barge
Wednesday 29th June
08.30 Coffee
Session Chair: Thierry Lecomte
09.00 Keynote 2: Denis Sabatier (ClearSy, France)
Using formal proof and B method at system level for industrial projects
Session: Systems 1. Chair: Aryldo Russo
10.00 Xiao Han, Tao Tang, JidongLv & Haifeng Wang (Beijing Jiaotong University, China)
Failure Analysis of Chinese Train Control System Level 3 Based on Model Checking
10.40 Coffee break
11.10 Marco Filax, Tim Gonschorek & Frank Ortmeier (Otto-von-Guericke-Universität, Germany)
Correct Formalization of Requirement Specifications: A V-Model for Building Formal Methods
11.50 Alexei Iliasov, Paulius Stankaitis & David Adjepon-Yamoah (University of Newcastle, UK)
Static verification of railway scheme and interlocking design data
12.30 Lunch
Session Chair: Alexander Romanovsky
13.30 Invited presentation: Claude Andlauer (Head of Rail Transport for RATP, France)
Formal methods as part of RATP’s DNA
Session: Systems 2. Chair: Véronique Delebarre
14.15 Christophe Limbrée, Quentin Cappart, Charles Pecheur (Université catholique de Louvain, Belgium)
& Stefano Tonetta (Fondazione Bruno Kessler, Italy)
Verification of railway interlocking – Compositional approach with OCRA
14.55 Coffee break
Session: Systems 3. Chair: Michael Leuschel
15.30 Paulius Stankaitis & Alexei Iliasov (CSR, Newcastle University, UK)
Safety Verification of Heterogeneous Railway Networks
16.10 Anne Elisabeth Haxthausen (Technical University of Denmark), Hoang Nga Nguyen (Centre for
Mobility and Transport, UK) & Markus Roggenbach (Swansea University, UK)
Comparing formal verification approaches of interlocking systems
16.50 Luke Martin (CSR, Newcastle University, UK)
Predictive Reasoning and Machine Learning for the Enhancement of Reliability in Railway Systems
17.30 Close of day 2
19.30 Conference Dinner – Le Train Bleu
Thursday 30th June
9.00 Coffee
Session Chair: Ralf Pinger
09.30 Keynote 3: Jan Peleska (University of Bremen & Verified Systems, Germany)
A novel approach to HW/SW integration testing of route-based interlocking system controllers
Session: V&V 1. Chair: Alessandro Fantechi
10.30 Daniel Kästner & Christian Ferdinand (AbsInt GmbH, Germany)
Applying Abstract Interpretation to Verify EN-50128 Software Safety Requirements
11.10 Coffee Break
11.40 Nazim Benaissa, David Bonvoisin, Abderrahmane Feliachi &
Julien Ordioni (RATP, France)
The PERF Approach for Formal Verification
12.20 Lunch
Session: V&V 2. Chair: Kenji Taguchi
13.20 Claire Dross & Yannick Moy (AdaCore, France)
Abstract Software Specifications and Automatic Proof of Refinement
14.00 Nicolas Breton & Yoann Fonteneau (Systerel, France)
S3: Proving the Safety of Critical Systems
14.40 Sylvain Conchon (Université Paris-Sud, France) & Mohammed Iguernlala (OCamlPro SAS, France)
Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo
15.20 Wrap-up and closing remarks
15.30 Close of Conference
