Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems.

Avionic systems involve complex time-dependent behaviors across interacting components. This paper presents a contract-based approach for formally verifying these behaviors in a compositional manner. A unique feature of our contract-based tool is the support of architectural specification for multi-rate platforms. An abstraction technique has also been developed for properties related to variable time bounds. Preliminary results on applying this approach to the verification of an aircraft cabin pressure control system are promising.