Model-Based Engineering for Avionics - Will Specification and Formal Verification Based on Broy's Streams - Become Feasible

Sep 18, 2026

Avionics software is a safety-critical domain where rising autonomy and real-time interactions increase complexity and create pressure to move beyond decades-old development practices. The paper argues for model-based specification within an integrated systems engineering approach, enabling formal, theorem-prover-based verification of physical and logical implementations against the specification. It demonstrates an early feasibility case using FOCUS, MontiArc ADL, and Isabelle on safety-critical real-time distributed systems.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages8

Reading Time20 min

AccessFree to download

Introduction

Background

Model-Based Engineering for Avionics: Will Speciﬁcation and Formal Veriﬁcation e.g. Based on Broy's Streams Become Feasible? Stefan Kriebel BMW Group Munich, Germany Deni Raco Chair of Software Engineering RWTH Aachen University Aachen, Germany Bernhard Rumpe Chair of Software Engineering RWTH Aachen University Aachen, Germany Sebastian St¨uber Chair of Software Engineering RWTH Aachen University Aachen, Germany Abstract—Avionics is deﬁnitely a safety-critical application domain. Software complexity is ever increasing together with more autonomy as well as increased real-time based interaction between airplanes, drones and potentially future air taxis. This again raises the question, whether developing software the same way as we did the last 30 years is still appropriate, or in the times of much better formal methods and cheap and powerful computational capabilities, it would be feasible to use clear and model-based speciﬁcation techniques for an integrated systems engineering approach and formally verify any physical and logical implementation of functionality, includingthe software against that speciﬁcation. This could be another important step towards quicker development of highly safetycritical systems. I. INTRODUCTION In this paper, we demonstrate early results on a small part of this systems engineering approach, namely using a userfriendly architecture description language [1], [2] and proving safety-critical properties in the theorem prover Isabelle [3] . Because the theory and its underlying methodological concepts are too much to be explained in this short paper, we highlight a small example only, focusing on the demonstration of the feasibility of formal veriﬁcation of complex software. Therefore, the paper demonstrates the use of the FOCUS framework [4]–[8] for specifying distributed interactive systems and verifying safety-critical properties of real-time critical software such as common in avionics systems. The methodology is modular with respect to composition. A userfriendly architecture description language (ADL) like MontiArc [1] serves as a developer frontend, allowing a state-based speciﬁcation of components [8] and enables the deﬁnition of the desired safety-critical properties. An appropriate tool maps the ADL model and its behavior speciﬁcations into speciﬁcations and theorems in the theorem prover Isabelle [3] . There, general composition operators exist that compose speciﬁcations of the components into a speciﬁcation of the overall system. Properties can be speciﬁed on a global scale and decomposed as well and proven on atomic components. Composition of properties leads to globally correct software. Furthermore, reﬁnement of a component in a decomposed structure automatically leads to reﬁnement of the composition, which allows to individually develop each component, but also to replace variants of implementations along the life cycle of a system. High-automation of the proofs, as well as the handling of feedback loops, unbounded non-determinism, time-sensitive speciﬁcations, safety and liveness properties, and reﬁnement checking are key for an efﬁcient development process. The rest of this paper is structured as follows: First, a motivation for the methodology is given. Then, the underlying theory is presented. Next, the tool chain consisting of the frontend DSL, the mathematical backend, and the generator is illustrated. Finally, the veriﬁcation of a property of the running example is demonstrated. II. BACKGROUND Designing distributed systems [6], [9] which react in realtime, are dependable and fulﬁll safety and liveness requirements, is a challenging problem [10] . Formulating requirements only in natural language is still common in the embedded industry and the challenging part is to early detect and avoid ambiguity [11] and inconsistencies [6] . In safetycritical systems errors might lead to injury or high costs as consequences [12] . For this reason, formal metho

FAQs

Why does the paper focus on model-based specification for avionics software?

Because avionics is safety-critical and software complexity grows with autonomy and real-time interaction, making it important to use clear specification techniques and formally verify implementations against them.

What frameworks and tools does the paper use for the demonstrated feasibility?

It uses the FOCUS framework for specifying distributed interactive systems, MontiArc as a developer frontend ADL, and Isabelle as the theorem prover backend to map models into specifications and theorems.

How is compositionality achieved when proving safety-critical properties?

The methodology supports modular composition: composition operators in Isabelle combine component specifications, properties can be specified globally and decomposed to atomic components, and refinement of components leads to refinement of compositions.

Sep 18, 2026

Uploaded by Taylor Morgan