Sprungmarken

Servicenavigation

       

Hauptnavigation

Bereichsnavigation

Hauptinhalt

BWInf-Workshop der TU Dortmund 2014

Model Checking

bla

Wieder einmal steht Omas Geburtstag vor der Tür und ein Geschenk ist nicht in Sicht. "Kein Problem", denkt sich der geübte Internetnutzer, "einfach schnell das Rätselbuch 2014 auf Banazon.de rausgesucht und auf 'Bestellen' geklickt, dann..."

Error 412. Object not available.

"Hmm..."

Das Erstellen fehlerfreier Software ist bekanntlich eine schwierige Aufgabe. Es wird nicht leichter, wenn viele Kundenanfragen gleichzeitig bearbeitet werden und die zugehörigen Prozesse zum Teil parallel und auf verschiedenen Servern arbeiten: Zur Abwicklung einer Bestellung muss zunächst die Lieferadresse abgefragt, das Geld vom Konto abgebucht und die Abbuchung bestätigt werden; anschließend müssen die Daten an das Lager geschickt werden, dieses muss den Lagerstand aktualisieren, gegebenenfalls zurückmelden, dass mittlerweile das Rätselbuch doch ausverkauft ist; schlussendlich muss der Kunde eine Benachrichtigung [1] bekommen. Nebenbei sollen tausende weitere Kunden zufriedengestellt werden.

Fehler in einer solchen Software können teuer werden. Wenn die Kaufabwicklung fehlerhaft ist, kaufen die Kunden bald woanders ein. Oder sie kaufen ein, ohne zu bezahlen... Formale Verifikation soll helfen, sicherzustellen, dass solche Fehler gefunden werden, bevor der Kunde sie findet. Und am besten nicht durch manuelles Testen, sondern automatisch und zuverlässig. Eine Methode der formalen Verifikation ist das Model Checking. Im Model Checking werden wichtige Eigenschaften, die ein System erfüllen soll, vorab beschrieben und anschließend ein Programm automatisch auf diese Eigenschaften überprüft.

In diesem Projekt soll überlegt werden, wie das Verhalten solcher Programme modelliert werden kann, in welcher Form gewünschte Eigenschaften beschrieben werden können und wie sich diese automatisch überprüfen lassen.

Voraussetzung ist Spaß an logischem Denken, Programmierkenntnisse sind nicht nötig.



  1. [1] Nach Möglichkeit nicht 'Error 412. Object not available.'

Letzte Änderung am 13.01.2014 von L. Pradel