Formal Verification of Flight Critical Software
Formal Verification of Flight Critical Software
复制标题
飞行关键软件的形式验证
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
M. Heimdahl
中科院分区：
文献类型：
--
作者：
Steven P. Miller;E. A. Anderson;Lucas G. Wagner;M. Whalen;M. Heimdahl
建模语言的最新进展使得正式指定和分析大型系统组件的行为是可行的。同步数据流语言，例如Luster，SCR和RSML非常适合此任务，并且SCADE和SIMULINK等这些工具的商业版本在安全关键系统的设计师中迅速增长，这在很大程度上是由于它们自动自动的能力从模型中生成代码。同时，正式分析工具的进步使得正式验证这些模型的重要特性是实用的，以确保在生命周期早期确定和纠正设计缺陷。该报告描述了如何将这种正式验证工具应用于FCS 5000，这是Rockwell Collins Inc.开发的一个新的飞行控制系统系列。
Recent advances in modeling languages have made it feasible to formally specify and analyze the behavior of large system components. Synchronous data flow languages, such as Lustre, SCR, and RSML are well suited to this task, and commercial versions of these tools such as SCADE and Simulink are growing rapidly in popularity among designers of safety critical systems, largely due to their ability to automatically generate code from the models. At the same time, advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This report describes how such formal verification tools have been applied to the FCS 5000, a new family of Flight Control Systems being developed by Rockwell Collins Inc.