Computergestützte Verifikation von Automatenkonstruktionen für Model Checking

• Applicants: Professor Dr. Javier Esparza; Professor Dr. Bernhard Nebel, since 9/2011; Professor Tobias Nipkow, Ph.D.
• Subject Area: Theoretical Computer Science
• Term: from 2010 to 2019
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 183790222

• Final Report Year: 2019

Final Report Abstract

Modelchecker sind ein wichtiges Werkzeug in der Softwareverifikation. Sie können für geeignet modellierte System automatisch entscheiden, ob diese eine gegebene Spezifikation erfüllen. Durch ihren breiten Einsatz und das große Vertrauen, das in sie gesetzt wird, ist es besonders wichtig, dass die Modelchecker selbst korrekt sind. Im Rahmen des CAVA Projekts wurde hierzu ein LTL Model Checker mit Hilfe des Theorembeweisers Isabelle formal verifiziert. Ergebnis des Projekts ist damit hauptsächlich die Formalisierung des CAVA Modelcheckers. Dabei ist eine Formalisierung eine Sammlung von Definitionen, Algorithmen, und Beweisen, wobei letztere vom Theorembeweiser Isabelle maschinell auf Korrektheit überprüft werden. Aus dieser Formalisierung lässt sich schließlich ausführbarer Code erzeugen, sodass der daraus resultierende CAVA Modelchecker als verifizierte Referenzimplementierung dienen kann. Es wurde auch eine Formalisierung der Promela Sprache erstellt, was die Nutzbarkeit des CAVA Model Checkers deutlich verbessert. Die Formalisierung stellt außerdem eine Spezifikation der Promela Semantik dar, was bis dato nur informell als Teil des SPIN-Buchs erfolgt war. Weiterhin wurden einige weitere Algorithmen formalisiert, die im Zusammenhang mit Graphen, Automaten, und Modelchecking stehen. Besonders hervorzuheben sind hier die Halbordnungsreduktion für Modelchecking, sowie die Reduktion mittels Färbung für Büchi Automaten. In beiden Fällen wurden im Zuge der Formalisierungsanstrengungen Fehler in den Algorithmen bzw. deren Korrektheitsbeweisen gefunden. Dies wiederum belegt die Notwendigkeit solcher Unternehmungen.

Publications

• Applying data refinement for monadic programs to Hopcroft’s algorithm. In Lennart Beringer and Amy P. Felty, editors, Interactive Theorem Proving (ITP), volume 7406 of LNCS. Springer, 2012
  Peter Lammich and Thomas Tuerk
  
• A fully verified executable LTL model checker. In N. Sharygina and H. Veith, editors, Computer Aided Verification (CAV), volume 8044 of LNCS. Springer, 2013
  Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus
  
• Using Promela in a fully verified executable LTL model checker. In Dimitra Giannakopoulou and Daniel Kroening, editors, Verified Software: Theories, Tools and Experiments, volume 8471 of LNCS. Springer, 2014
  René Neumann
  
• Verified efficient implementation of Gabow’s strongly connected component algorithm. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving (ITP), volume 8558 of LNCS. Springer, 2014
  Peter Lammich
  
• A framework for verifying depthfirst search algorithms. In Xavier Leroy and Alwen Tiu, editors, Certified Programs and Proofs (CPP). ACM, 2015
  Peter Lammich and René Neumann
  
• Büchi automata optimisations formalised in Isabelle/HOL. In Mohua Banerjee and Shankara Narayanan Krishna, editors, Logic and Its Applications (ICLA), volume 8923 of LNCS. Springer, 2015
  Alexander Schimpf and Jan-Georg Smaus
  
• Refinement to Imperative/HOL. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving (ITP), volume 9236 of LNCS. Springer, 2015
  Peter Lammich
  
• From LTL to deterministic automata - A safraless compositional approach. Formal Methods in System Design, 49(3):219–271, 2016
  Javier Esparza, Jan Kretínský, and Salomon Sickert
  
• Formal verification of an executable LTL model checker with partial order reduction. J. Autom. Reasoning, 60(1):3–21, 2018
  Julian Brunner and Peter Lammich