ETAPS Industry Day 2024

Formal Verification of Avionics Software

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).

What Programmers Want from Proof with SPARK

SPARK is an industrial programming language with a unique focus on program proof, adopted in domains where software safety or security is paramount. Since a reboot in 2014, the language has known continuous evolution to match what programmers in these domains want: strong guarantees at reasonable cost. To accommodate different cost/benefit choices, we have defined a scale of levels of assurance that define different guarantees and their cost. SPARK supports these levels with dedicated features both in the programming language and in the analysis tool. We will present how these features match what programmers want, where they fall short today, and what we are working on to reduce that friction in the future.

From Theory to Practice: What is a contract, really?

Contracts are agreements between multiple parties that contain obligations, prohibitions and permission to exchange specified quantities of scarce resources under various conditions and within certain time limits. A financial contract, roughly speaking, is a money-now-for-money-later exchange. They are the backbone and organizing principle of companies interacting with each other. But what are they, beyond their renditions ranging from short emails and taped conversations to voluminous prospectuses and term sheets in stylized legal prose rendered in Microsoft Word? Can they be formalized, capturing their operational semantics, not only digitized as template text instantiated with data records?

In this subjective talk we sketch the history of digitizing and eventually digitalizing (formalizing) commercial and financial contracts; highlight their relation and difference, both significant, to process calculi; argue why Ethereum-style programs are neither smart nor contracts despite being called smart contracts; and describe our work on formalizing contracts as a domain-specific language as part of a ‘revolutionary’ approach to enterprise resource planning (ERP) systems and its 20-year journey to application, commercialization and deployment in multiple capital markets systems that bridge traditional regulated finance with fully automated and transparent real-time finance without traditionally obligatory intermediaries.

Next Generation Model-based Testing for Industrial Applications

Model-based testing of safety-critical control systems has been a very active research field since the 1970s. A specialised branch of this field focused on the generation of so-called complete test suites. These guarantee a certain degree of fault coverage (e.g. language equivalence or property satisfaction), provided that certain hypotheses about the system under test are fulfilled. While having always been of high theoretical interest (black-box testing can really prove the absence of faults!), the practical applicability of complete test methods in industry has been successfully demonstrated within the last 15 years. Several companies - including Verified Systems - offer effective tool support for the model-based approach. It has to be admitted, however, that MBT tools have not become as successful as originally expected by researchers and tool providers. One of the root causes for this observation lies in the fact that ’typical’ software developers and testers prefer to program in C++, C#, Java, or Python to writing reference models in formalisms like UML, SysML, B, CSP and any other of the multitude of modelling formalisms advocated by the formal methods community. My own convictions about ’the best approach’ to test automation with guaranteed test strength, as well as the tool-oriented strategy of Verified Systems have therefore changed significantly within the last two years. (1) We are convinced that module-level testing should be performed by specifying properties and verifying them by means of test-based model learning in combination with model checking. (2) Integration testing and system-level testing should be performed by specifying system-level properties and an expert-driven, rule-based approach to create ‘meaningful’ end-to-end tests. (3) Guaranteed fault coverage should be the goal on module-level testing, while the higher levels rather require end-to-end tests that are ‘convincing’ for the certification authorities. In this presentation, I will focus on the first aspect (module testing) and demonstrate how the original ideas about ‘black-box checking’ by Peled, Vardi, and Yannakakis have been refined recently and made fit for industrial application. This is achieved by using more effective model learning techniques in combination with fuzz testing and monitors detecting the violation of safety properties. Moreover, static analysis techniques allow for the verification of hypotheses about the module under test, so that passing a test suite is really equivalent to a mathematical proof that the software correctly implements the required properties. Finally, a cloud-based tool platform allows for effective test suite creation, execution, and management of test-related artefacts.

European RD Projects: Participation and Opportunities

In this presentation, I will talk about different European funding opportunities for research and innovation projects. The main focus will be on Horizon Europe, EU’s flagship funding framework program, covering fundamental research all the way to market uptake. For that, I will introduce the fundamental structure of Horizon Europe and its eligibility, as well as details about upcoming topics in AI/ML and cybersecurity, where formal methods could be directly applied. With background in Computer Science, I currently work at Luxinnovation, the national innovation agency of Luxembourg, in the role of National Contact Point and Program Committee member on digital/ICT and cybersecurity topics.