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.
Presenter: David Delmas, Airbus, Fr
Date: 16 January, 15.00-16.00 (CET)
Zoom: to be announced
Title: Formal Verification of Avionics Software
Abstract: The size and complexity of avionics software have grown exponentially from one aircraft generation to the next in the past 4 decades. Traditional software development processes leveraging informal verification techniques fail to scale within reasonable costs. In particular, verification is liable for a steadily growing share of the overall development costs. The 2015 current status was about 70%. To address this issue, Airbus have been transforming internal development processes since 2016. Internal domain-specific languages have been developed to enable the formalization of design artifacts, and automate part of verification activities. Automation is enabled by the interoperation of tools relying on sound formal techniques. For instance, Frama-C/WP and SMT-solvers are used to automate unit verification with deductive methods. Most so-called Unit Proofs are automatic, assuming high-level memory and numerical models, as well as some preconditions. Such assumptions are verified by other tools, such as the Astrée static analyzer, which leverages Abstract Interpretation to prove the absence of run-time errors and check assumed non-aliasing properties. We rely on the CompCert formally verified compiler to enable that most formal verification activities may be conducted on source code. Beyond safety properties and currently established processes, we also develop internally static analyses by Abstract Interpretation to automate regression verification and portability verification. In particular, our portability analysis is able to prove without false alarms the portability of low-level C avionics software up to 1 million lines of C across platforms with opposite byte-orders (endianness).
Bio: David Delmas has been working as an avionics software engineer at Airbus since 2001. He specializes in methods and tools, with a strong focus on formal verification. He has contributed to the transfer of research prototypes into the development workshops of operational avionics software teams since 2007. These tools include the Astrée and Fluctuat static analyzers, and the Frama-C platform. They are currently used as part of the verification processes of safety-critical avionics software products. He completed a PhD thesis on the static analysis of program portability by abstract interpretation in 2022, as part of his work at Airbus.
Presenter: Leo Freitas, ScubaTx, UK
Date: 3 October, 16.00-17.00 (CEST)
Zoom: https://mdu-se.zoom.us/j/68372371873?pwd=hhYzv1Y0CHY12C078u72uEMbGbCauB.1
Title: Digital Twins for Organ Preservation Devices
Abstract: Digital Twins (DTs) are a promising technology for integrating device monitoring and data consumption to improve performance. This technology has seen utilisation in various industries that use cyber-physical systems. An unexpected area is medical devices. In this paper, we explore DTs use for an organ preservation device, which, helps improve transplantation outcomes by actively managing the organ during transport to prevent biological degradation. Whilst reducing the burden on specialists. Digital twinning offers an exciting direction of development for medical devices to improve transplantation outcomes.
Bio: Leo is a Senior Lecturer in Formal Methods and Tools and Newcastle University (UK) with 25 years experience in safety-critical systems development involving model based design, formal specification, model checking and theorem proving. He has applied these techniques to industrial scale in various areas like avionics (AeroEngines, Praxis) , transportation, payment systems (e.g. EMV, MasterCard, Mondex), cyber security and medical. For the last 10 years, Leo has worked on various embedded medical devices and is the Co-Founder and CIO of an organ preservation start-up (ScubaTx) since 2020.
Presenter: Daniel Fredholm, Prover Technology, Sweden
Date: 16 May, 15.00-16.00 (CEST)
Video: See the recording of the Zoom meeting (the first few minutes are missing due to technical problems; our apologies)
Title: Formal Verification in the Railway Domain
Bio: Daniel got his PhD in mathematics in 1994 (mathematical logic) from Stockholm University, Sweden, and has been employed at Industrilogik (1996-2005), and at Prover Technology since 2005. Daniel has extensive expertise in formal methods, in particular formal verification, applied to rail control systems.
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.