Korrektheit durch formale Methoden - Bianca Lutz, Lars Hupel

Software Testing - Qualität, Testautomatisierung & Agilität

Mathematik meets Software-Qualität

"Mit Tests kann ich Fehlerfreiheit nicht nachweisen. Es gibt einfach bestimmte Domänen, da brauche ich aber die Fehlerfreiheit und eben auch den Nachweis." - Lars Hupel, Bianca Lutz

In der neuesten Episode des Software Testing Podcasts feiern wir die World Quality Week. Ich spreche mit mit Lars und Bianca darüber, wie man Fehlerfreiheit in Software mathematisch beweisen kann und welche Tools dabei helfen. Bianca erklärt uns anhand von Beispielen aus der Finanz- und Automobilbranche, warum bestimmte Systeme absolute Fehlerfreiheit benötigen. Lars ergänzt das Gespräch mit Einblicken in formale Methoden und wie sie in der Praxis angewendet werden. Ein besonders interessantes Thema war, wie KI uns bei der Beweisführung unterstützen kann.

Lars Hupel ist Chefevangelist für digitale Währungen bei Giesecke+Devrient, einem internationalen Unternehmen für Sicherheitstechnologie. Im Rahmen dieser Tätigkeit hält und schreibt Lars zahlreiche Vorträge, Workshops und Artikel, um die Technik hinter Digitalwährungen einem breiten Publikum zugänglich zu machen. Mit einem Hintergrund als Softwareentwickler trägt Lars aber auch zur Produktentwicklung bei und vertritt das Unternehmen bei verschiedenen Industriegremien. Lars hat im Bereich Logik und Verifikation an der TU München promoviert und bringt diese Erkenntnisse ein, um die Produkte von Giesecke+Devrient noch sicherer zu machen.

Bianca Lutz ist Softwarearchitektin bei der Active Group GmbH und arbeitet von Berlin aus. Schon im Studium interessierte sie sich für formale Methoden und hat mit dem Beweisassistenten Isabelle/HOL gearbeitet. Aber auch technische Themen, wie Betriebssysteme und hier vor allem eingebettete Systeme, begeistern sie bis heute. Sie war an verschiedenen wissenschaftlichen Publikationen beteiligt, ist Linux-Kernel-Contributor und hat im Rahmen ihrer Abschlussarbeit in Isabelles Archive of Formal Proofs veröffentlicht. Nach mehrjähriger Tätigkeit in der Versicherungsbranche, bei der sie es vor allem mit Legacy-Code zu tun hatte, wechselte sie 2022 ins Lager der Funktionalen Programmierung über.

Highlights:

• In Bereichen wie Finanzen und Medizin ist Fehlerfreiheit entscheidend, und formale Methoden können dabei helfen.
• Formale Methoden nutzen mathematische Modelle und Beweisassistenten, um Softwarefehler zu vermeiden.
• Microsoft nutzt automatisierte Tools, um Treiber auf Fehlerfreiheit zu überprüfen.
• Formale Methoden sind keine Allheilmittel, sondern ergänzen andere Testmethoden.
• Änderungen in der Software können zu aufwendigen Anpassungen in den Beweisen führen.

Links:

• https://lars.hupel.info/
• https://www.linkedin.com/in/lars-hupel
• https://mastodon.hupel.info/@lars
• https://www.linkedin.com/in/bianca-l-53a013220/
• https://www.software-testing.fm

Danke an die Community-Partner des Podcasts:

• Alliance for Qualification: https://swt.fm/a4q
• ASQF: https://swt.fm/asqf
• Austrian Testing Board: https://swt.fm/atb
• dpunkt.verlag: https://swt.fm/dpv
• German Testing Board: https://swt.fm/gtb
• German Testing Day: https://swt.fm/gtd
• GI Fachgruppe TAV: https://swt.fm/tav
• Heise: https://swt.fm/hei
• HANSER Verlag: https://swt.fm/chv
• ISTQB: https://swt.fm/ist
• iSQI GmbH: https://swt.fm/isqi
• oop: https://swt.fm/oop
• QS-TAG: https://swt.fm/qst
• SIGS-DATACOM: https://swt.fm/sigs
• skillsclub: https://swt.fm/sc
• Software Quality Days: https://swt.fm/swqd
• Swiss Testing Board: https://swt.fm/stb

Credits:

• Sound: https://swt.fm/krz
• Grafik: https://swt.fm/kdb

Kapitel

1. Einführung und Begrüßung (00:00:00)

2. Formale Methoden in der Qualitätssicherung (00:01:06)

3. Praktische Anwendung formaler Methoden (00:08:04)

4. Einführung in formale Methoden (00:12:02)

5. Verifizierung von CompCert (00:13:01)

6. KI-Unterstützung bei formalen Beweisen (00:22:03)

7. Einführung in klassische KI und formale Methoden (00:23:47)