From Design Contracts to Component Requirements Verification
This addresses the challenge of requirement verification in avionics systems development, providing an automated solution that supports certification, though it appears incremental as it builds on existing modeling and verification environments.
The paper tackles the problem of manual translation of requirements between different development environments in complex airborne systems by presenting a tool-supported export technique that translates high-level requirements into observers for verification, enabling efficient compliance checks and an automated tool chain consistent with avionics certification guidance, as demonstrated on a medical infusion pump and an aircraft wheel braking system.
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.