Development and Formal Verification of a Flight Stack for a High-Altitude Micro Glider (Masterthesis)
14.02.2017,14:00 room 4981
The ubiquitous demand for intelligent control systems increases the amount of micro-processors and the size of their software. To minimize the probability of critical system failures, software verification is becoming more important than ever. In contrast to classical testing and simulation, formal methods are able to prove the absence of errors. However, formal methods are considered to be complicated, require manual interaction, and are often only performed when the implementation is completed. In this thesis, we investigate and propose a development process to integrate formal verification as a parallel process during natural, incremental software development. For this purpose, a flight stack for a high-altitude micro glider was developed and verified with the SPARK toolsuite from Adacore. We started with a classical design of the software architecture based on requirements and afterwards implemented the software in SPARK. During implementation, we added code annotations on demand and verified the absence of run-time errors in parallel. We also applied common safety concepts for high-integrity software and analyzed implications on the formal verification process. As a result, we were able to formally prove the absence of 87% of possible run-time errors and the correctness of 98% of functional contracts in analyzed subprograms. The formal analysis covered 82% of our own subprograms and 44% of all subprograms (including third-party libraries). Furthermore, we formally proved the dimension correctness of physical calculations. The parallel verification process helped to identify faults prior to compile time but also introduced limitations to the implementation possibilities. Our field experiments revealed that formal verification could replace classical unit tests, but are not sufficient to replace system tests that run the software under real-world conditions.