Kugelsichere Architektur mit formalen Methoden

Korrektheit, eigentlich eine selbstverständliche Anforderung an Software, schafft es selten in die offizielle Design-Dokumentation. Aber: Manche Software *muss* korrekt sein – solche, die kritische Hardware steuert, besonders sensible Informationen schützt oder umsatzkritische Berechnungen anstellt.

Tests allein können Korrektheit nicht sicherstellen, dafür braucht es formale Beweise. Ein ganzes Arsenal von Techniken und Werkzeugen hilft, Korrektheitsbeweise zu erstellen und zu überprüfen. Soll eine Architektur diese Techniken unterstützen, ist allerdings Sorgfalt geboten, insbesondere beim Design verifizierbarer Modelle. Der Vortrag gibt einen Überblick darüber, wie Software verifiziert werden kann und wie die Architektur dafür entworfen wird — anhand von Fallbeispielen aus der Praxis.