飞行关键系统的安全性评估
Verifying the Safety of a Flight-Critical System
摘要：
本文介绍了我们的工作演示验证技术的飞行关键系统的现实功能，大小和复杂性。我们的工作针对一个商用飞机控制系统命名为运输类模型（TCM），并涉及几个阶段：形式化和消除歧义的要求，与主专家合作;处理模型，他们使用的形式化验证工具;应用组合技术在体系结构和组件级别的规模验证。在一个重要的NASA里程碑的背景下进行，这项研究的形式化验证在实践中是最具挑战性的，我们的团队已经执行，它花了几个人月来完成it. This本文介绍了我们遵循的方法和我们学到的教训。
英文摘要：
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 do- main 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, and it took several person months to complete it. This paper describes the methodology that we followed and the lessons that we learned.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
