Umfang

Dieses Thema kann als Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • sicherheitskritische Systeme
  • B / Event-B
  • Prolog, Java

Problemstellung

Die Grundlage der meisten Werkzeuge für die formale Verifikation sind Constraint Solver. ProB bietet unter anderem einen mächtigen Constraint Solver für die B und Event-B Sprache. Außerdem gibt es verschiedene Backends zu anderen SMT Solvern wie z.B. Z3. Bei dem Constraint sowie SMT Solving werden explizite Modelle für erfüllbare Formeln und Gegenbeispiele für nicht erfüllbare Formeln berechnet. Für die formale Verifikation in B und Event-B sind explizite Modelle oder Gegenbeispiele oft wichtig, z.B. für die Animation von formalen Modellen. Teilweise wird jedoch nur die Information benötigt ob eine Formel erfüllbar ist oder nicht, z.B. für Beweise der Induktivität von Invarianten oder bei dem symbolischen Model Checking. Automatische Theorembeweiser verwenden vereinfacht gesagt clevere Umschreiberegeln sowie bestehende Axiome um die Erfüllbarkeit von Formeln zu widerlegen. Die Erfüllbarkeit einer Formel kann hierbei durch initiale Negation bewiesen werden. Ein Vorteil automatischer Theorembeweiser ist, dass keine expliziten Modelle berechnet werden müssen und somit z.B. keine Domänen von Variablen enumeriert werden müssen. Hierbei ist anzumerken, dass die Domänen von Variablen ggf. unbeschränkt sind und eine vollständige Enumeration somit nicht zielführend ist. Eine Annahme ist daher, dass automatische Theorembeweiser insbesondere bei dem Widerlegen von unerfüllbaren Formeln über Variablen mit unbeschränkten Domänen vorteilhaft gegenüber Constraint oder SMT Solvern sind. Eine übliche Eingabesprache für automatische Theorembeweiser ist die TPTP Sprache.

Im Rahmen dieser Arbeit soll die B und Event-B Sprache nach TPTP übersetzt werden, so dass B und Event-B Formeln mittels externen automatischen Theorembeweisern bewiesen oder widerlegt werden können. Genauer gesagt ist wahrscheinlich die THF0 Sprache am besten geeignet. Die Übersetzung soll mittels ProB automatisiert werden. Hierfür bietet sich eine Implementierung in ProB’s Prolog Kern an. Alternativ ist eine Implementierung mithilfe der ProB Java API in einer JVM-basierten Programmiersprache denkbar. Als externe Theorembeweiser sollen unter anderem Isabelle sowie Zipperposition verwendet werden. Nach erfolgreicher Implementierung (einer Teilmenge) der B und Event-B Sprache soll ein Performancevergleich zwischen ProB’s Constraint Solver, ProB’s SMT Solver Backends und dem neuen Theorembeweiser Backend vollzogen werden.

Minimalanforderungen

  • Übersetzung einer Teilmenge von B und Event-B in die TPTP Sprache (THF0)
  • Integration in ProB
  • Unit-, Integrations- und Fuzzingtests
  • Performanceauswertung

Erweiterungen

  • Performanceoptimierung

Kontakt

Joshua Schmidt
Raum 25.12.02.52 · joshua.schmidt@hhu.de