@inproceedings{90c93a63ed9f4d64b14fad0761bb201a,
title = "Development and verification of a flight stack for a high-altitude glider in Ada/SPARK 2014",
abstract = "SPARK 2014 is a modern programming language and a new state-of-the-art tool set for development and verification of high-integrity software. In this paper, we explore the capabilities and limitations of its latest version in the context of building a flight stack for a high-altitude unmanned glider. Towards that, we deliberately applied static analysis early and continuously during implementation, to give verification the possibility to steer the software design. In this process we have identified several limitations and pitfalls of software design and verification in SPARK, for which we give workarounds and protective actions to avoid them. Finally, we give design recommendations that have proven effective for verification, and summarize our experiences with this new language.",
keywords = "Ada/SPARK, Formal verification, Limitations, Rules",
author = "Martin Becker and Emanuel Regnath and Samarjit Chakraborty",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 36th International Conference on Computer Safety, Reliability, and Security, SAFECOMP 2017 ; Conference date: 13-09-2017 Through 15-09-2017",
year = "2017",
doi = "10.1007/978-3-319-66266-4_7",
language = "English",
isbn = "9783319662657",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "105--116",
editor = "Friedemann Bitsch and Stefano Tonetta and Erwin Schoitsch",
booktitle = "Computer Safety, Reliability, and Security - 36th International Conference, SAFECOMP 2017, Proceedings",
}