Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems
Devesh Bhatt, Arunabh Chattopadhyay, Wenchao Li, David B. Oglesby, Sam Owre, Natarajan Shankar · Lecture notes in computer science · 2016
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. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.