Verification And Validation In Railway Using Formal .

Using Formal Methods forVerification and Validation in RailwayKlaus Reichl

Klaus.Reichl@gmail.comComputer Hacker and Guitar PlayerLiving in ViennaKlaus.Reichl@thalesgroup.comSystem and Software ArchitectHandelskai 92A-1200 esgroup.com/austria2

Outline Railway Theory - The Norm A “Real” Model Excurse: ERTMS, ETCS and InterlockingModelling Formally Railway in ActionRailway Theory - The Standards Excurse: CENELEC StandardInterlocking Architecture and its ModelWhat comes next Plans for the near FutureKlaus Reichl - Formal Methods for Verification and Validation in Railway3

Bad Aibling 2016Klaus Reichl - Formal Methods for Verification and Validation in Railway4

Bad Aibling 2016 - Facts Head to head collision at 100 km/h eachTrains were equipped with the PZB (Punktförmige Zugbeeinflussung) train protectionsystem ( Indusi) Enforces line-side signaling and prevent drivers from accidentally pass signals in case ofdanger Main signals showing “stop” or are out of operation can be passed when subsidiary signalsoperated by the train dispatcher are setBoth trains received permission by means of a subsidiary signal due to human error150 people were on the trains, considerably fewer than normal because of Holidayseason 12 people died, 85 others were injuredKlaus Reichl - Formal Methods for Verification and Validation in Railway5

Excurse: CENELEC NormKlaus Reichl - Formal Methods for Verification and Validation in Railway6

CENELEC - a standard for (not only) RailwaysCENELEC/TC 9X is responsible for the development of European Standards forElectro Technical Applications related to the Rail Transport Industry of theEuropean Union. CENELEC is European (AREMA is the American counterpart)CENELEC includes Development Process beside RAMS and Hardware CENELEC EN 50128 Railway applications - Communications, signalling and processing systemsspecialises EN 61508 Functional Safety of Electrical/Electronic/Programmable Electronic Safety-related SystemsKlaus Reichl - Formal Methods for Verification and Validation in Railway7

CENELEC railway standards for signallingEN 50126-1 :1999: The specification and demonstration of reliability, availability,maintainability and safety (RAMS).EN 50128:2011: Software for railway control and protection systems. Replaced2001 version.EN 50129:2003: Safety-related electronic systems for signalling. Replaced 1998version.EN 50159:2010: Safety-related communication in transmission systems. Replaced2001 version.Klaus Reichl - Formal Methods for Verification and Validation in Railway8

Safety Integrity Level Concept of Safety Integrity Level (SIL) based on the Tolerable Hazard RateSIL 4 is the most stringentTolerable Hazard RateTHR per hour and functionSafety Integrity Level (SIL). 10-9 THR 10-8410-8 THR 10-7310-7 THR 10-6210-6 THR 10-5110-5 THR 10-3 .0Klaus Reichl - Formal Methods for Verification and Validation in Railway9

The V-Model in CENELECKlaus Reichl - Formal Methods for Verification and Validation in Railway10

The V-Model in CENELEC - PhasesKlaus Reichl - Formal Methods for Verification and Validation in Railway11

The V-Model in CENELEC - MissionsKlaus Reichl - Formal Methods for Verification and Validation in Railway12

CENELEC Recommendations Formal Methods are “recommended” for SIL 1/2 and “highly recommended”for SIL 3/4 Formal Proof is “recommend” for SIL 1/2 and “highly recommended” for SIL3/4 Software Requirement Specification (Table A.2)Software Architecture (Table A.3)Modelling (Table A.17)Verification and Testing (Table A.5)Formal Proof of correctness of data is “highly recommended” for SIL 3/4 Data Preparation Techniques (Table A.11)Klaus Reichl - Formal Methods for Verification and Validation in Railway13

CENELEC on Formal Methods apply formal methods to requirements and high-level designs where most ofthe details are abstracted awayapply formal methods to only the most critical componentsanalyse models of software and hardware where variables are made discreteand ranges drastically reducedanalyse system models in a hierarchical manner that enables "divide andconquer"automate as much of the verification as possibleDescribed are CSP, CCS, HOL, LOTOS, OBJ, Temporal Logic, VDM, Z, B, ModelChecking and Formal ProofKlaus Reichl - Formal Methods for Verification and Validation in Railway14

CENELEC Tools QualificationSOI - System of Interest SIL Level Qualification and AssessmentEnabling System Tool Qualification, part of the Assessment T3 - Tools which produces code or data for SOI T2 - Tools which are used to verify and validate the SOI Test and Verification ToolsT1 - Other tools in the development process Code and Data GeneratorsEditorsGrey Zone - Build Tools, Statistics, .TVR (Tool Validation Report) as framework to Qualification ProcessKlaus Reichl - Formal Methods for Verification and Validation in Railway15

Back to modelling .Klaus Reichl - Formal Methods for Verification and Validation in Railway16

All Models are WrongGeorge Box 1976(https://en.wikipedia.org/wiki/All models are wrong#cite note-1). but Some are UsefulGeorge Box 1978Klaus Reichl - Formal Methods for Verification and Validation in Railway(https://en.wikipedia.org/wiki/All models are wrong#cite ref-2)17

Since all models are wrong. the scientist cannot obtain a "correct" one by excessiveelaboration. On the contrary following William of Occam heshould seek an economical description of natural phenomena.Just as the ability to devise simple but evocative models is thesignature of the great scientist so overelaboration andoverparameterization is often the mark of mediocrity.George Box 1976Klaus Reichl - Formal Methods for Verification and Validation in Railway18

All Models are Right. Most are UselessThaddeus Tarpey 2012Klaus Reichl - Formal Methods for Verification and Validation in th/211/)19

Fallacy of ReificationWhen an abstraction (the model) is treated as if it were a realconcrete entity. The fallacy of reification is commited over and over,believing the model represents the truth. instead of anapproximation. The model is not wrong but treating the model as theabsolute truth (i.e. reification) is wrong.Thaddeus Tarpey 2012Klaus Reichl - Formal Methods for Verification and Validation in Railway20

Model of a Classical InterlockingKlaus Reichl - Formal Methods for Verification and Validation in Railway21

22

23

Questions? Is the model right? Is the model useful? Is the model economically practical?Klaus Reichl - Formal Methods for Verification and Validation in Railway24

No Routes?No Station?No Flank Protection?Train Length?Train Integrity?Klaus Reichl - Formal Methods for Verification and Validation in Railway25

Questions? Is the model right? Is the model useful? Is the model economically practical?Klaus Reichl - Formal Methods for Verification and Validation in Railway26

Classical Signalling Conventional Optical Signals Optional Train ProtectionRoute Control - pre configured Priority Routes Alternative RoutesTrains (rather vehicles!) detected by Track CircuitElement Control Points and SignalsKlaus Reichl - Formal Methods for Verification and Validation in Railway27

Questions? Is the model right? Is the model useful? Is the model economically practical?Klaus Reichl - Formal Methods for Verification and Validation in Railway28

Is the Model Economically Practical? Great Demo for Customers (Little & Big Girls) Way too expensive Maintenance by “Ferro-Sexual” Hobbyists Not shareable Not movable However a small variant exists ;-)Klaus Reichl - Formal Methods for Verification and Validation in Railway29

Excurse: Some words on ERTMS, ETCSand InterlockingKlaus Reichl - Formal Methods for Verification and Validation in Railway30

ERTMS - European Rail Traffic Management SystemEuropean Union driven replacement to the different nationaltrain control and command systems in Europe. GSM-R (Global System for Mobiles - Railway) Communication between vehicles and line controllersETCS (European Train Control System) In-cab train control supplementing or replacing trackside signaling Interface to InterlockingsETML (European Traffic Management Layer) Operation management level to optimize train movements Augmentation to Interlockings by means of Remote Control andTraffic/Operational Management CentresKlaus Reichl - Formal Methods for Verification and Validation in Railway31

ETCS - European Train Control Level 0 - ETCS-fitted vehicles on non-ETCS route Level 1 - Cab signalling which can be superimposed on the existing signalling system Eurobalise radio beacons pick up signal aspects from the trackside signals via signal adapters and telegramcoders (STM - Specific Transmission Module)“Infill” Eurobalise or EuroLoop between the distant signal and main signal deliver new proceed aspectsLevel 2 - Cap signalling via digital radio-based system (Radio Block Center - RBC) Train driver observes tracksideMight be limited in speed by the last balises encounteredMovement Authority and other signal aspects are granted via radioBreaking curves implemented by the Onboard Unit (EVC - European Vital Computer)Level 3 - From Train Protection to full Radio-Based Train Spacing Trains find their position themselvesFixed blocks (potentially) replaced by Moving Blocks (breaking distance spacing)Reliable Train Integrity (End of Train device)Klaus Reichl - Formal Methods for Verification and Validation in Railway32

ETCS - European Train Control Level 0 - ETCS-fitted vehicles on non-ETCS route Level 1 - Cab signalling which can be superimposed on the existing signaling system Eurobalise radio beacons pick up signal aspects from the trackside signals via signal adapters and telegramcoders (STM - Specific Transmission Module)“Infill” Eurobalise or EuroLoop between the distant signal and main signal deliver new proceed aspectsLevel 2 - Cap signalling via digital radio-based system (Radio Block Center - RBC) Train driver observes tracksideMight be limited in speed by the last balises encounteredMovement Authority and other signal aspects are granted via radioBreaking curves implemented by the Onboard Unit (EVC - European Vital Computer)Level 3 - From Train Protection to full Radio-Based Train Spacing Trains find their position themselvesFixed blocks (potentially) replaced by Moving Blocks (breaking distance spacing) Reliable Train Integrity (End of Train device)Klaus Reichl - Formal Methods for Verification and Validation in RailwayGraphic: https://en.wikipedia.org/wiki/European Train Control System33

ETCS - European Train Control Level 0 - ETCS-fitted vehicles on non-ETCS route Level 1 - Cab signalling which can be superimposed on the existing signalling system Eurobalise radio beacons pick up signal aspects from the trackside signals via signal adapters and telegramcoders (STM - Specific Transmission Module)“Infill” Eurobalise or EuroLoop between the distant signal and main signal deliver new proceed aspectsLevel 2 - Cap signalling via digital radio-based system (Radio Block Center - RBC) Train driver observes tracksideMight be limited in speed by the last balises encounteredMovement Authority and other signal aspects are granted via radioBreaking curves implemented by the Onboard Unit (EVC - European Vital Computer)Level 3 - From Train Protection to full Radio-Based Train Spacing Trains find their position themselvesFixed blocks (potentially) replaced by Moving Blocks (breaking distance spacing)Reliable Train Integrity (End of Train device)Klaus Reichl - Formal Methods for Verification and Validation in RailwayGraphic: https://en.wikipedia.org/wiki/European Train Control System34