Scaling Correctness-by-Construction

In sicherheitskritischen Domänen wie dem Automobil-, Flug- und Medizinsektor haben Software-Systeme hohe Sicherheitsanforderungen, da Softwarefehler in solchen Systemen Menschenleben gefährden können. Standardmäßig kommen hier Techniken aus dem Bereich der formalen Methoden, insbesondere die Post-hoc-Verifikation, zum Einsatz. Dabei wird ein Programm zunächst vollständig implementiert und formal spezifiziert und erst anschließend auf seine funktionale Korrektheit verifiziert. Ein großer Nachteil von Post-hoc-Verifikation ist, dass Fehler nur schwer lokalisiert werden können, da es an einer strukturierten Vorgehensweise zur Konstruktion der Programme mangelt. ... mehrDas führt dazu, dass der Code und die Spezifikation oft willkürlich verändert werden, bis sich das Programm schließlich (möglicherweise) verifizieren lässt. Idealerweise kommt es aber gar nicht erst zu einem solchen Trial-and-Error-Vorgehen, wenn ein Entwicklungsansatz verwendet wird, der das Spezifizieren und Verifizieren direkt in den Entwicklungsprozess integriert und somit zu einer korrekten Lösung hinleitet.
Correctness-by-Construction (CbC) integriert Spezifikation und Verifikation in einen inkrementellen Entwicklungsprozess. Ausgehend von einer formalen Spezifikation in Form einer Vor- und Nachbedingung wird das Programm schrittweise zu einer als korrekt beweisbaren Implementierung verfeinert. Dabei wird jeder Verfeinerungsschritt auf seine Korrektheit überprüft. Die Vorteile von CbC sind, dass durch den inkrementellen Prozess Fehler früher entdeckt werden und dass Entwickler:innen dem entwickelten Programm mehr vertrauen, da es in einem formalen Prozess erstellt wurde. Erste Experimente mit dem Tool CorC, welches CbC unterstützt, zeigen eine erhöhte Verifikationseffizienz im Vergleich zu Post-hoc-Verifikation. Dennoch wurde CbC bislang nur zur Entwicklung einzelner Algorithmen angewendet. Moderne Software ist jedoch größer und komplexer und wird in Teams mit verschiedenen Expertisen entwickelt. Das Ziel dieser Dissertation ist es daher, CbC für die Entwicklung im modernen Software-Engineering anwendbar zu machen. Insbesondere fokussiert sich diese Dissertation auf vier konkrete Herausforderungen: 1) Strukturelle Komplexität durch Objekt-Orientierung, 2) Integration in etablierte Softwareentwicklungsprozesse, 3) eine hohe Einstiegshürde durch fehlende Verifikationsexpertise und 4) fehlende Unterstützung von fortgeschrittenen Programmierparadigmen, wie zum Beispiel für hochkonfigurierbarer Software.
In dieser Dissertation werden drei Kernbeiträge vorgestellt, die die zuvor genannten Herausforderungen adressieren. Im ersten Kernbeitrag wird CbC um ein Objektmodell erweitert, welches Klassen, Felder, Methoden, Vererbung, Klasseninvarianten und Methodenframes integriert. Darüber hinaus wird ein Roundtrip Engineering Prozess entwickelt, der die Integration von CbC in etablierte Softwareentwicklungsprozesse sowie die Kombination mit weiteren Qualitätssicherungsmethoden ermöglicht. Im zweiten Kernbeitrag wird die Einstiegshürde für Entwickler:innen mit geringen Vorkenntnissen im Bereich der Softwareverifikation verringert. Dazu wird Testen als Zwischenstufe zwischen Spezifizieren und Verifizieren in einem dreistufigen Entwicklungsprozess integriert. Testen ist eine weitverbreitete Qualitätssicherungsmethode, die leicht verständliche Testberichte liefert und somit eine schnelle Fehlersuche und -behebung ermöglicht. Der zweite Kernbeitrag wird hinsichtlich seiner Effektivität, Fehler zu lokalisieren, sowie hinsichtlich Verbesserungsmöglichkeiten der Nutzbarkeit unseres Tools evaluiert. Der dritte Kernbeitrag erweitert CbC um die Entwicklung von hochkonfigurierbarer Software, welche Variabilitätsmechanismen nutzt, um eine komplette Softwarefamilie effizient zu implementieren. Daher wird CbC um Variabilitätskonstrukte in der Spezifikation, den Programmkonstrukten und den Verifizierungsstrategien erweitert. Die vorgestellten Konzepte werden auf ihre Korrektheit hin bewiesen. Des Weiteren wird eine Machbarkeitsevaluation durchgeführt und die Beweiseffizienz der vorgestellten Verifizierungsstrategien ermittelt. Darüber hinaus wird überprüft, welcher Zusammenhang zwischen dem Spezifikationsaufwand und der Beweiseffizienz besteht, indem CbC mit Post-hoc-Verifikation verglichen werden. Zusammenfassend ermöglichen die vorgestellten Kernbeiträge eine Anwendung von CbC in objekt-orientierten und hochkonfigurierbaren Softwaresystemen, die mit etablierten Softwareentwicklungsprozessen und von Entwickler:innen mit variierender Expertise im Bereich Softwareverifikation entwickelt werden.

As software in safety-critical systems, such as automotive, aviation, and medical systems, grows in complexity, stronger correctness guarantees beyond traditional testing are essential, as faults may endanger human lives. Typically, the functional correctness of such systems is ensured with post-hoc verification, which means that a program is verified after it has been completely implemented and specified with a pre- and postcondition contract. Usually, automated program verifiers are used for post-hoc verification. A major drawback of post-hoc verification is the lack of construction guidance, making fault localization difficult when verification fails. ... mehrFaults may result from incorrect implementations, insufficient specifications, or unclosable proofs, leading to trial-and-error adjustments in the specification and code. Ideally, with a guided approach to construct correct software, the developer would think about the problem first rather than a concrete implementation and is then guided towards a correct solution without trial-and-error adjustments.
Correctness-by-Construction (CbC) integrates specification and verification into an incremental development process. Starting from a formal specification as an abstract Hoare triple, programs are progressively refined into verified implementations, checking the correctness of each refinement step. CbC provides benefits, such as early error detection and increased trust in the software through the structured development process. CbC is implemented in the tool CorC and first experiments with CorC show an increased proof efficiency compared to post-hoc verification for small algorithms. Despite these benefits, CbC has still mostly been applied to isolated algorithms. However, in modern software engineering, complex, large-scale software systems are developed in teams with different expertise. In particular, we identified four key challenges for applying CbC in modern software engineering: 1) structural complexity through object-orientation, 2) integration into existing development processes, 3) a high entry barrier due to limited verification expertise of developers, and 4) lack of support for advanced programming paradigms, such as those for highly configurable software systems.
In this thesis, we made three contributions that address these four challenges to extend CbC such that it is applicable in modern software engineering. First, we scale CbC to support object-oriented systems by introducing an object model with classes, fields, methods, inheritance, class invariants, and frames enabling encapsulation, inheritance, polymorphism, and dynamic dispatch. A roundtrip engineering process enables integration into established software development processes, such that CbC development can be combined with other quality assurance techniques. Second, to lower the entry barrier of using CbC for non-experts in software verification, we integrate a three-level process of increasing correctness guarantees that incorporates testing as an intermediate level between specifying and verifying. Since testing is a well-known quality assurance technique, developers get understandable test reports and can locate and fix major errors early in the design phase. We evaluate the three-level process quantitatively to assess its efficiency in locating faults and qualitatively to asses usability improvements. Third, we extend CbC to support highly configurable software systems. The challenge of highly configurable software systems is that they incorporate variability to enable the efficient development of whole product families. Therefore, we incorporate variability in the specification, the code constructs, and the verification strategies of CbC. We prove the soundness of these variability concepts and evaluate feasibility and proof efficiency of the verification strategies. Furthermore, we want to assess whether there is a trade-off between specification effort and proof efficiency when comparing CbC and post-hoc verification. Overall, our work enables CbC to be applied for object-oriented software and highly configurable software systems within software teams with varying expertise levels that use established software development processes.