From Design Contracts to Component Requirements Verification

TL;DR

This paper introduces a tool-supported method for translating high-level system requirements into verifiable observers within software components, streamlining verification and ensuring compliance in complex airborne systems.

Contribution

It presents an automated export technique and tool chain that enable formal verification from system requirements to low-level software, aligned with avionics certification standards.

Findings

Effective verification demonstrated on a medical infusion pump.

Automated tool chain supports formal verification processes.

Ensures compliance with avionics certification guidance.

Abstract

During the development and verification of complex airborne systems, a variety of languages and development environments are used for different levels of the system hierarchy. As a result, there may be manual steps to translate requirements between these different environments. This paper presents a tool-supported export technique that translates high-level requirements from the software architecture modeling environment into observers of requirements that can be used for verification in the software component environment. This allows efficient verification that the component designs comply with their high-level requirements. It also provides an automated tool chain supporting formal verification from system requirements down to low-level software requirements that is consistent with certification guidance for avionics systems. The effectiveness of the technique has been evaluated and demonstrated on a medical infusion pump and an aircraft wheel braking system.