Umfang

Diese Arbeit kann im Rahmen einer Projekt - oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • gute Kenntnisse in Prolog (z.B. durch Besuch der Veranstaltung “Logische Programmierung”)
  • Kenntnisse in Compilerbau (z.B. durch Besuch der Veranstaltung “Compilerbau”) sind hilfreich
  • Kenntnisse der B/Event-B Sprache (z.B. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”) sind hilfreich

Problem

POs werden dazu genutzt um die Korrektheit (Abwesenheit von ungewünschtem Verhalten) in einem formalen Model zu beweisen. Bisher werden POs in den Tools Atelier-B und Rodin unterstützt, womit sich B bzw. Event-B Modelle beweisen lassen. Rodin-Handbuch

ProB ist ein Animator und Model Checker der am Lehrstuhl entwickelt wird. Mit ProB kann man unter anderem B und Event-B Modelle animieren und model checken und auf diese Weise validieren bzw. verifizieren.

Die Aufgabe dieser Arbeit besteht darin einen PO Generator für B und Event-B zu implementieren, und ProB zu integrieren. Insbesondere sollen POs aus B und Event-B Modellen generiert werden, sodass die in ProB vorhandenen Solver versuchen können diese zu lösen. Mögliche Erweiterungen der Arbeit sind u.a. interaktives Beweisen von POs, sowie die Einbindung von POs in ProB2-UI.

B und EventB sind formale Modellierungssprachen, mit welchen wir mathematisch beweisbar korrekte Software entwickeln können.

Generell (und reduziert) gesprochen bestehen EventB Maschinen je einen Initialzustand und eine Menge an Operationen/Events, welche den Zustand ändern. Desweiteren gibt es Invarianten (logische Aussagen über den aktuellen Zustand), welche immer erfüllt sein müssen.

Um zu garantieren, dass ein Event gefahrlos ausgeführt werden kann, müssen vorher entsprechende POs bewiesen werden.

Als Beispiel diene eine Maschine mit der Invariante x > 0 und dem Initialzustand x := 3. Betrachten wir nun das folgende Event

event decx begin
  x := x-1
end

welches x um eins Reduziert. Eine Beweisobligation wäre zu zeigen, dass x > 0 => x-1 > 0 gilt; und zwar für alle möglichen x. (In diesem Beispiel ist die Beweisobligation nicht erfüllbar; Gegenbeispiel ist x=1.)

Minimalanforderungen

  • funktionsfähige Generierung von POs für B und Event-B Modelle
  • funktionsfähige Anbindung an vorhandene Solver und Beweiser

Erweiterungen

  • Übersichtliche Darstellung der POs
  • ausführliche Evaluation der Performance
  • Einbindung von interaktivem Beweisen von POs
  • Einbindung an ProB2 bzw. ProB2-UI

Kontakt


Sebastian Stock
Sebastian.Stock@jku.at
Fabian Vu
Raum 25.12.02.50
Fabian.Vu@hhu.de