Invited Talks

The conference programme will include invited talks by:

  • Robin Bloomfield from Adelard LLP and City University London: The risk assessment of ERTMS based railway systems from a cyber perspective: methodology and lessons learnt.

Robin E Bloomfield is a founder of the specialist safety and security consultancy Adelard LLP.  He is also Professor of System and Software Dependability at City University London where he leads a project as part of the UK National Research Centre on Trustworthy ICS (RiTICS). His work in safety and security in the past 30yrs has combined policy formulation, technical consulting and underpinning research. He was elected a Fellow of the Royal Academy of Engineering in 2014 in recognition of his international leadership in the engineering of safety-critical systems containing software.

Abstract.

The impact that cyber issues might have on the safety and resilience  of railway systems  has been studied for nearly a decade by industry specialists and government agencies. This talk/paper presents some of the work lead by Adelard starting with an analysis of vulnerabilities in ERTMS specifications through to a high level preliminary system risk assessment followed by detailed analyses of particular systems on behalf of UK industry.  The focus of the paper will be on the issue of security informed safety, the development of cyber informed hazard analyses and overall methodology. High level results will be presented but of course many details remain proprietary or sensitive and cannot be published.

  • Denis Sabatier from ClearSy: Using formal proof and B method at system level for industrial projects.

Denis Sabatier is one of the co-founders of ClearSy, a French company that specializes in safety critical systems, both for consultancy and specific system design. The domain of ClearSy notably includes railway safety specific systems (some of them are currently in service in Paris metro line 1 and 13) and railway safety critical CBTC software. Mr Sabatier participated since 1995 in the development of the B-method and the Atelier-B tookit and their application for different projects, in particular CBTC railway projects. Since 2010, Mr Sabatier has been the leader of several projects devoted to formal proofs at system level.

Abstract.

Since several years, ClearSy has driven large projects about using formal proofs at system level. The fundamental goal in these projects is to extract the rigorous reasoning that establishes that the considered system ensures its requested properties, and to assert that this reasoning is correct and fully expressed. In this paper, we give feedback about the methodology used in all these projects, about the differences made by whether the concerned system is currently under design or already existing and about the benefits obtained. The formal proofs are performed using Event-B, with the Atelier-B toolkit. 

  • Claude Andlauer from RATP, France: Formal methods as part of RATP’s DNA.

After 5 years spent on oceano-metorological systems, Claude committed the last 24 years of his career to railway system engineering, participating in major international railway transportation projects, involving managerial and technical responsibilities, from both supplier and operators perspectives (at SNCF, ALSTOM and now RATP) At present, Claude is leading Transportation Systems Engineering division at RATP (public transport company in Paris, France). This division being in charge of signaling and train control systems engineering and project delivery for Paris urban and suburban network extension and renovation.

  • Jan Peleska from University of Bremen and Verified Systems: A novel approach to HW/SW integration testing of route-based interlocking system controllers.

Jan Peleska is co-founder of Verified Systems International GmbH, a company dedicated to the development of tools and the provision of services in the field of safety-critical system development, verification, validation and test. Since 1995, Dr. Peleska is professor for computer science (operating systems and distributed systems) at the University of Bremen in Germany. Before that, he worked with Philips and other companies as Senior Software Designer and later on as department manager in the field of fault-tolerant systems, distributed systems, and safety-critical embedded systems.  His current research interests include formal methods for the development of dependable systems and test automation with applications to embedded real-time systems. Current industrial applications of his research work focus on the development and verification of avionic software, space mission systems, and railway and automotive control systems. 

Abstract.

Recent progress in bounded model checking and inductive reasoning has shown that the fully automated verification of route-based interlocking system designs of realistic "real-world" complexity is possible and ready for industrial application. In this paper, we present a new model-based testing strategy for interlocking system controllers that exploits the fact that the design has already been verified, so that it can be used as a reference model for test case and test oracle generation. Our special interest lies in the field of complete testing strategies that are able to uncover every implementation error, provided that the implementation behaviour is captured in a pre-specified fault domain. Despite their guaranteed test strength, these strategies have two well-known disadvantages: (1) applied in a naive way, they often result in an infeasible amount of test cases, and (2) the hypothesis that the real implementation behaviour is captured by a member of the fault domain can rarely be justified in a convincing way. We describe a new combination of compositional reasoning and input equivalence class generation techniques that removes problem (1). For coping with disadvantage (2), we suggest a combination of equivalence class and random testing that - while not being able to guarantee complete fault coverage for implementations outside the fault domain - results in a test strength that is significantly higher than heuristic test approaches for interlocking system controllers. Estimates are presented that show how application of this novel strategy reduces the effort for HW/SW integration testing, while simultaneously increasing the fault coverage in comparison to more conventional testing approaches.