This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft control system named Transport Class Model (TCM), and involved several stages: formalizing and disambiguating requirements in collaboration with domain experts; processing models for their use by formal verification tools; applying compositional techniques at the architectural and component level to scale verification. Performed in the context of a major NASA milestone, this study of formal verification in practice is one of the most challenging that our group has performed.
CITATION STYLE
Brat, G., Bushnell, D., Davies, M., Giannakopoulou, D., Howar, F., & Kahsai, T. (2015). Verifying the safety of a flight-critical system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9109, pp. 308–324). Springer Verlag. https://doi.org/10.1007/978-3-319-19249-9_20
Mendeley helps you to discover research relevant for your work.