Invited Talks
Challenges for safe and secure CPS
Thierry Lecomte
— Research Director at ClearSy
Aix-en-Provence (France)
CPSs populate our environment and interact with us on a daily basis. Some are in charge of our safety, all are potential targets for attackers. Formal methods make it possible to take into account certain dimensions of analysis during the design of CPSs but also during their operation. This presentation aims at presenting the current situation in the field of land transportation and at highlighting the difficulties encountered as well as the challenges ahead.
With a background in robotics and AI, Thierry was deeply involved in signal processing (at large) and pattern recognition applications (both civil and military). For the first automatic metro deployed in Paris, he was in charge of improving Atelier B proof performances through the development of theorem provers.
Being one of the 4 founders of his company, CLEARSY, he has been committed to the dissemination and rational use of formal methods in industry (railways, energy, space, healthcare, microelectronics, etc.)
As such, he has been at the origin, in charge, or involved in 24 Regional, French, and European R&D projects during the last 22 years.
Lately he was granted the development, exploitation, and dissemination of the CLEARSY Safety Platform, a certified generic safe computer able to reach the highest safety levels for command and control settings. He is currently working to protect the systems developed by CLEARSY from cybersecurity risks.
Recent advances for hybrid systems verification with HyPro
Erika Ábrahám
— Professor at RWTH Aachen
Aachen (Germany)
Hybrid systems are systems with mixed discrete-continuous behavior. Despite intensive research during the last decades to offer algorithms and tools for the reachability analysis of hybrid systems, the available technologies still suffer from scalability problems.
Though scalability can be increased on the cost of precision, it is not easy to find the right balance that leads to successful verification in acceptable time. In this talk we give a general introduction to hybrid systems and methods for their reachability analysis, introduce our HyPro tool, and report on some recent work to speed up the computations while still maintaining sufficient precision.
Erika Ábrahám graduated at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the development and application of deductive proof systems for concurrent programs. After a postdoc time at the Albert-Ludwigs-University Freiburg (Germany), since 2008 she is professor at RWTH Aachen University (Germany), with main research focus on formal methods for probabilistic and hybrid systems as well as SMT solving for real and integer arithmetic.
Reachability analysis and simulation for hybridised Event-B models.
Paulius Stankaitis
— Research Associate Professor at Newcastle University
Newcastle-upon-Thyne (UK)
The development of cyber-physical systems has become one of the biggest challenges in the field of model-based system engineering. The difficulty stems from the complex nature of cyber-physical systems which have deeply intertwined physical processes, computation and networking system aspects. To provide the highest level of assurance, cyber-physical systems should be modelled and reasoned about at a system-level as their safety depends on a correct interaction between different subsystems.
In this talk we present a development framework of cyber-physical systems which is built upon a refinement and proof based modelling language – Event-B and its extension for modelling hybrid systems. To improve the level of automation in the deductive verification of the resulting hybridised Event-B models, the presentation we describe a novel approach of integrating reachability analysis in the proof process.
Furthermore, to provide a more comprehensive cyber-physical system development and simulation-based validation, we describe mechanism for translating Event-B models of cyber-physical systems to Simulink.
Paulius is a Research Associate Professor at Newcastle University (UK). Paulius obtained a PhD from Newcastle University from in September 2021. His research focuses on the development of techniques and tools for modelling and formal verification of cyber-physical systems, particularly, autonomous vehicles and railway signaling systems.