基于状态Transformers元语言的航天器控制程序形式化验证
Formal Verification of Spacecraft Control Programs Using a Metalanguage for State Transformers
摘要：
验证控制程序的功能正确性是开发空间电子设备的一项基本任务;它既困难又耗时，而且在开发时间方面通常超过设计和编程任务。我们提出了一种验证方法，旨在帮助航天器工程师减少所需的努力，形式化验证的低级别控制程序上执行的自定义硬件。该方法使用元语言将程序的语义描述为一个状态转换器Transformer，可以编译为多个目标，用于测试、形式化验证和代码生成。元语言本身嵌入在强类型宿主语言（Haskell）中，提供了一种在类型级别证明程序属性的方法，可以缩短反馈循环，进一步提高工程师的生产力。验证方法是证明了一个工业案例研究。我们提出的REDFIN，在空间任务中使用的处理核心，其正式的语义表示使用建议的元语言，其次是一个简单的控制程序的验证的详细例子。
英文摘要：
Verification of functional correctness of control programs is an essential task for the development of space electronics; it is difficult and time-consuming and typically outweighs design and programming tasks in terms of development hours. We present a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of low-level control programs executed on custom hardware. The approach uses a metalanguage to describe the semantics of a program as a state transformer, which can be compiled to multiple targets for testing, formal verification, and code generation. The metalanguage itself is embedded in a strongly-typed host language (Haskell), providing a way to prove program properties at the type level, which can shorten the feedback loop and further increase the productivity of engineers. The verification approach is demonstrated on an industrial case study. We present REDFIN, a processing core used in space missions, and its formal semantics expressed using the proposed metalanguage, followed by a detailed example of verification of a simple control program.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
