In association with Formal Methods Europe (FME)
Watch the video
Download the presentation slides (PDF)
Synopsis
Advances in formal methods tools have enabled a wide variety of new ways of using formal models and for increasing the added value of formal modelling. In this talk I will present my experience in using the B formal method for systems modelling and data validation in the railway sector. I will start out by situating the B-method within the realm of formal methods, and provide a brief overview of twenty-five years of industrial usage. I will then discuss various lessons learnt during my experience with formal methods, in particular for the new hybrid-level 3 European train control system specification. I will discuss how to combine the various verification and validation aspects, from proof to visualization, leading to new applications such as executable prototypes or interactive requirements documents.
About the speaker
Michael Leuschel is full professor at the Institut für Informatik of Heinrich-Heine-Universität Düsseldorf, Germany, where he leads the Software Engineering and Programming Languages group. His research focusses on model-based problem solving using symbolic model checking.
He has been one of the main developers of ProB, a successful animator, constraint solver and model checker for the B-Method. ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard. Michael’s research is also behind the development of the ECCE system for partial deduction.
Our events are for adults aged 16 years and over.
This event is brought to you by: Formal Aspects of Computing Science (FACS) specialist group in association with Formal Methods Europe (FME)
