观测卫星星载自主功能验证的形式化方法
软件工程
2020-02-11 v1 计算机科学中的逻辑
摘要
我们提出了一种对地球观测卫星功能行为进行建模的新方法。我们利用该方法开发了一款安全关键软件——"遥控指令验证器"，负责在星上检查指令序列是否安全可执行。为了增加卫星的自主性，需要这一新服务。为此，我们提出了一种新的领域特定建模语言以及集成到嵌入式软件所需的工具链。该框架基于带有安全条件、超时以及接受时长作为参数的转移的确定性有限状态机的组合。它能够从卫星的高层规约生成同步编程语言 Lustre 的代码。这给出了一种形式化方法，用以推导基于事件的算法来模拟遥控指令序列的执行，并由此得到一个可证明正确的星上验证器。
引用
@article{arxiv.2001.11875,
title = {Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites},
author = {Vincent Mussot and Silvano Dal Zilio and Loic Correnson and Serge Rainjonneau and Yves Bardout and Grégoire Scano},
journal= {arXiv preprint arXiv:2001.11875},
year = {2020}
}