The InFM series, organised by the FME Industry Committee, is a series of talks in which industrial practitioners using Formal Methods in their development take the stage and offer some rare insights into the benefits and potential pitfalls of applying Formal Methods in their domain.
The talks are aimed at people working in industry wishing to learn from others applying Formal Methods at industrial scale, but also academics interested in applying and improving their methods.
Past talks:
Presenter: Frank Zeyda, Galois Inc. (US) and Independent Contractor
Date: 22 February, 16.00-17.00 (CET)
Video: See the recording of the Zoom meeting (the first few minutes are missing; our apologies)
Title: Rigorous Digital Engineering with Formal Methods: a personal perspective
Abstract: Rigorous Digital Engineer (RDE) is a methodology and process to create trustworthy, safe and secure hardware and software systems `from the ground up’. It permeates the entire life-cycle of traditional hardware, software and firmware engineering, from requirements and domain models to product-line descriptions, architectural specifications, component and unit design, and implementation. Each life-cycle stage is accompanied by meaningful models that support formal analysis, refinement, validation and verification activities, so that models at different levels of abstraction remain strongly connected to each other in a mathematical sense.
RDE has formed the basis of many projects at Galois, Inc. that require the highest levels of assurance, targeting embedded encryption devices, applications in avionics, space and defense, and secure voting systems - just to name a few. Despite this, the methodology and process of RDE has only recently been clearly articulated, as an adaptable process and methodology that can cater for a large class of heterogeneous systems, from pure software to pure hardware and anything in between.
In this presentation, I will reflect on my personal understanding, experience and view of RDE, and its relationship to the use of Formal Methods and underlying tool support. This entails both my academic experience working on novel formal modeling and verification strategies, i.e., for control, embedded, and cyber-physical systems, and industrial experience working closely with Galois to help advocate, shape and apply their RDE vision as a methodology in its own right.
Short Bio: Frank Zeyda obtained his PhD in 2007 from Teesside University (UK) and has subsequently worked for many years in academia, mainly at the University of York (UK) to conduct fundamental research towards novel verification techniques and strategies for control systems, Safety-Critical Java, and FMI cosimulation for cyber-physical systems. As part of this work, he has also extensively contributed to the embedding of semantic theories into theorem provers, with a focus on Tony Hoare’s Unifying Theories of Programming (UTP). Since 2018, he has dedicated himself mainly to industrial work to gain experience in applying rigorous and innovative verification and testing strategies to real-world applications in avionics, namely for the Verified Systems Int. GmbH in Germany. As of 2022, he acts as an independent consultant and researcher living in Mexico, currently working closely with Galois, Inc. He specializes in the application of formal methods and their tools towards creating more reliable, trustworthy and secure hardware and software.
Presenter: Ivo ter Horst, ASML.
Date: 28 September, 15.00-16.00 (CET)
Video: See the recording of the Zoom meeting.
Title: Test less, verify Moore – Formal verification at ASML.
Abstract: ASML’s lithography machines are complex cyber-physical systems of systems, designed to be extremely accurate, deliver very high throughput and operate 24/7 to deliver exceptionally reliable results. More than 10 years ago, ASML embarked on a formal verification journey to transform its software development practices with the aim of improving software quality and speeding up delivery.
In this talk, we will present how we apply formal verification, using tooling provided by a commercial partner and highlight some of the challenges faced when doing this on an industrial scale. Today, millions of lines of code generated from formally verified models make ASML systems run reliably.