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.
CITATION STYLE
Bhatt, D., Chattopadhyay, A., Li, W., Oglesby, D., Owre, S., & Shankar, N. (2016). Contract-based verification of complex time-dependent behaviors in avionic systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9690, pp. 34–40). Springer Verlag. https://doi.org/10.1007/978-3-319-40648-0_3
Mendeley helps you to discover research relevant for your work.