Verification of C++ Flight Software with the MCP Model Checker
Verification of C++ Flight Software with the MCP Model Checker
复制标题
使用 MCP 模型检查器验证 C Flight 软件
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
G. Brat
中科院分区：
文献类型：
--
作者：
S. Thompson;G. Brat
美国宇航局的星座项目要求设计一个乘员探索飞行器（猎户座，也称为CEV）和货物运载火箭（战神，也称为CLV）。这两个项目都将依赖于新设计的飞行控制软件。这些C++飞行代码的验证是至关重要的，特别是对猎户座来说，因为人类的生命将处于危险之中。有一些商业工具用于验证C++代码。然而，没有一个商业上可用的工具能很好地发现处理并发的bug。然而，猎户座和战神的软件都被期望是多线程的。通过这项工作，我们建议通过开发一套可用于验证C++代码的工具来解决这个问题。我们的工具将从一个静态分析器（基于抽象的解释，如C Global Surveyor）的模型检查器（MCP，我们在本文中介绍），包括一个符号执行引擎的测试用例生成（TPGEN）。本文主要研究MCP及其在航天软件中的应用。
The Constellation project at NASA calls for designing a crew exploration vehicle (Orion, also called CEV) and cargo launch vehicle (Ares, also called CLV). Both projects will rely on newly designed flight control software. The verification of these C++ flight codes is critical, especially for Orion, since human life will be at stake. There exist some commercial tools for the verification of C++ code. However, none of the commercially available tools does a good job at finding bugs dealing with concurrency. Yet both software for Orion and Ares are expected to be multi-threaded. With this work we are proposing to address the issue by developing a suite of tools that can be used to verify C++ code. Our tools will range from a static analyzer (based on abstract interpretation like C Global Surveyor) to a model checker (MCP, which we present in this paper) including a symbolic execution engine for test case generation (TPGEN). This paper focuses on MCP and its application to aerospace software.