一项使用ACSL与Frama-C表述并验证符合DO-178C的航空项目底层需求的实验研究
软件工程
2015-08-20 v1 计算机科学中的逻辑
摘要
安全关键的航空电子软件是形式化验证的自然应用领域。这体现在形式化方法被纳入认证指南DO-178C及其形式化方法补充DO-333中。例如，空客和达索航空已开展使用形式化验证的研究。德国大型国家研究项目Verisoft XT也考察了形式化方法在航空领域的应用。然而，形式化方法尚未成为主流，并且形式化验证（尤其是形式化演绎）能否被集成到资源受限的中小企业（SME）的软件开发过程中值得怀疑。总部位于慕尼黑的中型公司ESG开展了一项小型实验研究，在真实航空项目的一小部分上应用形式化验证。某软件功能的底层规范使用ACSL形式化，相应源代码使用Frama-C及WP插件配合自动化证明器Alt-Ergo进行了部分验证。我们确立了几条方法需满足以适合中小企业工业使用的标准，并利用在真实世界示例中结合ACSL与Frama-C所获得的经验对这些标准进行了评估。本文报告了该研究的成果，同时也强调了该方法在总体上的一些问题，这些问题中，我们认为在嵌入式实时编程领域使用该方法时通常会遇到。
引用
@article{arxiv.1508.03894,
title = {An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project},
author = {Frank Dordowsky},
journal= {arXiv preprint arXiv:1508.03894},
year = {2015}
}
备注
In Proceedings F-IDE 2015, arXiv:1508.03388