Umfang

Dieses Thema kann als Bachelorarbeit oder Teil einer Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • gute Prolog Kenntnisse (z.B. durch Besuch der Veranstaltung “Einführung in die logische Programmierung”)
  • Grundkenntnisse im Compilerbau
  • Kenntnisse der B Sprache sind erwünscht (zB. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)

Problem

B ist eine Methode zur formalen Spezifikation und Analyse von Software-Systemen. Die B-Methode nutzt Mengentheorie und Prädikatenlogik für die formale Beschreibung des Systems. Mit dem am Lehrstuhl entwickelten Tool ProB können Systeme, die in B oder Event-B spezifiziert wurden, analysiert und validiert werden. Man kann zum Beispiel automatisch überprüfen, ob ein B-Modell mit endlichem Zustandsraum seine Invariante erfüllt, indem man den ProB Model Checker benutzt.

Im Laufe der Entwicklung des formalen Modells können Prädikaten (z.B. in der Invariante oder in den Guards der Operationen des B-Modells) entstehen, die ausdruckslose bzw. redundante Teile haben. Als Beispiel kann man das folgende Prädikat nehmen:

P = pc2 < n & (pc1 = n & pc2 + 1 = n)

In P kann man das Prädikat ‘pc2<n’ als redundant betrachten, da P genau dann wahr ist, wenn ‘pc1=n’ und ‘pc2 = n-1’ gelten, und ‘n-1 < n’ immer gilt. Mit anderen Worten man kann P zu ‘pc1=n & pc2 + 1 = n’ vereinfachen. Andere einfache Beispiele wären ‘x<2 => y=y’ (kann zu ‘TRUE’ vereinfacht werden) oder ‘!x.(x:NATURAL => x>1)’ (kann zu ‘FALSE’ umgeformt werden).

Das Auftreten von solchen Prädikaten beansprucht in vielen Fällen unnötige Berechnungen bei der Evaluierung dieser Prädikate. In dieser Hinsicht entsteht unnötiger Aufwand beim Model-Checking des entsprechenden Modells sowie bei der Anwendung von Optimierungstechniken für den Model Checker wie Partial Order Reduction oder Partial Guard Evaluation.

Ziel dieser Arbeit ist ein Simplifier für Prädikate in B und Event-B zu entwickeln. Der Simplifier soll in Sicstus Prolog implementiert werden.

Als Referenz kann man das Paper ‘Automatic Flow Analysis for Event-B’ [1] nehmen. Neben der Publikation der Arbeit ‘Automatic Flow Analysis for Event-B’ wurde ein Prototyp entwickelt, der beim Einstieg in das Thema helfen kann. Zusätzlich kann man die Rewriting Rules, die in Rodin implementiert sind, als Referenz für die Implementierung des Simplifiers benutzen: wiki.event-b.org/index.php/All_Rewrite_Rules.

Minimalanforderungen

  • funktionsfähiger Simplifier für eine Untermenge von B
  • Analyse der Fähigkeiten auf ein paar Beispielen, Vergleich mit ProB

Erweiterungen (für Masterarbeit erforderlich)

  • Erweiterung der abgedeckten Sprache
  • Ausführliche empirische Evaluierung und Einbindung in ProB

Kontakt

Professor Michael Leuschel
Raum 25.12.02.60 · michael.leuschel@hhu.de