微小型飞行器应急恢复系统的软件验证方法
软件工程
2017-06-12 v2
摘要
本文描述了一种用于微小型飞行器（Micro Air Vehicles）的竞争性降落伞系统的开发与验证，特别关注嵌入式软件的验证。我们首先介绍整体解决方案，包括系统级故障分析，然后展示如何最小化故障软件的影响。本文证明，通过谨慎的抽象和少量的过近似，在微处理器上运行的整个代码可以使用有界模型检测（bounded model checking）进行验证，并且这对于资源受限的嵌入式系统是一种有用的方法。由此产生的应急恢复系统据我们所知是同类中首个通过形式化验证的系统，并且从操作角度看优于所有其他现有解决方案（包括商用方案）。
引用
@article{arxiv.1506.07867,
title = {Approaches for Software Verification of an Emergency Recovery System for Micro Air Vehicles},
author = {Martin Becker and Markus Neumair and Alexander Söhn and Samarjit Chakraborty},
journal= {arXiv preprint arXiv:1506.07867},
year = {2017}
}
备注
12 pages, 34th International Conference on Computer Safety, Reliability and Security (SAFECOMP)