基于 Ada/SPARK 2014 的高空滑翔机飞行栈的开发与验证
软件工程
2017-07-05 v1
摘要
SPARK 2014 是一种现代编程语言，也是开发和验证高完整性软件的最新先进工具集。在本文中，我们在为高空无人滑翔机构建飞行栈的背景下，探讨了其最新版本的的能力和局限性。为此，我们在实施过程中故意早期且持续地应用静态分析，以使验证能够指导软件设计。在此过程中，我们识别了 SPARK 中软件设计和验证的几个局限性和陷阱，并给出了避免它们的变通方法和保护措施。最后，我们给出了已被证明对验证有效的设计建议，并总结了我们使用这种新语言的经验。
引用
@article{arxiv.1707.00945,
title = {Development and Verification of a Flight Stack for a High-Altitude Glider in Ada/SPARK 2014},
author = {Martin Becker and Emanuel Regnath and Samarjit Chakraborty},
journal= {arXiv preprint arXiv:1707.00945},
year = {2017}
}