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.

Value for the audience:
Die Teilnehmer:innen bekommen Informationen über formale Methoden: Welche Methoden und Techniken gibt es, wie lassen sie sich in den Software-Entwicklungsprozess integrieren und was leisten sie?

Problems addressed:
Wie lässt sich funktionale Korrektheit feststellen?

Wie lässt sich funktionale Korrektheit sicherstellen?

Talk language: German
Level: Advanced
Target group: Software-Architekt:innen, Software-Entwickler:innen, Tester:innen

Company:
Active Group GmbH

Bianca Lutz

Dr. Lars Hupel