Trusting Outsourced Components In Flight Critical Systems
Falk Maria Howar, Temesghen Kahsai, Arie Gurfinkel, Cesare Tinelli · 2015
A common practice in the development of complex component-based flight critical software systems is to outsource the implementation of some of the components to external contractors or assemble them from commercial off-the-shelf (COTS) systems. Those components are delivered as black-box systems, although they may have been first prototyped in-house by the system integrator. In this paper we present our idea to formally analyze flight critical software that has been assembled from COTS or outsourced for implementation. Our approach is based on contract-based compositional verification. Specifically, we propose a two-stage approach with a pre-delivery and a post-delivery verification stage. In the first stage, verification focuses on generating contracts, a widely used method for organizing the integration of component-based systems, for the outsourced component. Contracts specify the precise information needed to reason about a component’s interaction with other parts of the system as well as system-level properties. In the second stage, outsourced components or COTS must be checked for conformance to the pre-specified formal contract. This stage involves two types of testing: contract-based component (unit) testing and contract-based system (integration) testing. To illustrate our approach, we provide two case studies of flight-critical systems.