Kugelsichere Software mit formalen Methoden

Manche Software hat klar formulierbare kritische Anforderungen, die so wichtig sind, dass im Fehlerfall Köpfe rollen. Typischerweise geht es dabei um Leib, Leben, geheime Daten oder einfach nur um große Umsätze.

Formale Methoden liefern mathematische Beweise, dass die Software solche Anforderungen garantiert erfüllt. Dafür werden die entsprechenden Eigenschaften – insbesondere was die Security betrifft – in den Code aufgenommen und von speziellen Werkzeugen (mit menschlicher Hilfe) verifiziert.

Die Anwendung dieser Techniken benötigt Vorbereitungen in der Softwarearchitektur, von denen aber auch andere Aspekte der Softwareentwicklung profitieren. Der Vortrag gibt einen Überblick darüber, wie formale Methoden funktionieren, was sie möglich machen und wie sich Menschen und Projekte für ihren Einsatz vorbereiten können

Vorkenntnisse

• Erfahrung in Softwareentwicklung
  
• Erfahrung in Software-Qualitätssicherung

Lernziele

• Einschätzen können, was formale Methoden leisten können
  
• Einschätzen können, ob der Einsatz formaler Methoden im eigenen Projekt sinnvoll ist
  
• Ressourcen kennen für die Vorbereitung eines Einsatzes formaler Methoden