Formal Object-oriented Software Development: The Whole Picture

• Applicants: Professor Dr. Bernhard Beckert; Professor Dr. Peter H. Schmitt
• Subject Area: Software Engineering and Programming Languages
• Term: from 2006 to 2011
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 22995750

• Final Report Year: 2015

Final Report Abstract

Um Softwareentwicklung durch Einsatz formaler Methoden voranzubringen, setzte sich das Open Door-Projekt folgende Ziele: Formale Methoden müssen wichtige Aspekte der Programmierpraxis abdecken, wie Nebenläufigkeit. Formale Methoden müssen integriert werden, sowohl miteinander als auch mit dem industriellen Entwicklungsprozess. Diese Ziele wurden, wie folgt, erreicht. Wir stellten eine neuartige Programmlogik vor, um Zusicherungen über die Korrektheit von Thread-basierten Programmen zu machen, und einen Kalkül (basierend auf symbolischer Ausführung), um diese Zusicherungen zu beweisen. Die Logik und der Kalkül zeichnen sich durch ihre gute Verständlichkeit für den Anwender aus. Ein Prototyp wurde im KeY-System implementiert. Es wurde ein Ansatz entwickelt und implementiert, der Techniken der automatischen statischen Programmanalyse zum Behandeln von Schleifen in den deduktiven Verifikationsansatz integriert. Das Generieren der Invariante und die sonstige Deduktion finden dabei innerhalb desselben logischen Kalküls statt. Es handelt sich insofern um eine tiefergehende Integration, die es vermeidet, Wissen über semantische Domänen oder die Programmiersprachensemantik mehrfach modellieren zu müssen. Da Modularität unabdingbar für Verifikation in der Praxis ist, wurde ein Konzept zur Übertragung der Dynamic Frames-Theorie in die Logik des KeY-Systems erarbeitet und implementiert. Es wurde ein Ansatz entwickelt und als Eclipse-Plug-In implementiert, der die während einer Beweissuche akkumulierte Information im Stile eines Debuggers zugänglich macht. Insbesondere liefert dieses System dem Benutzer nach einem fehlgeschlagenen Beweisversuch durch visuelle Markierungen im Quellcode des zu verifizierenden Programmes Hinweise auf mögliche Fehlerursachen. Die Einsicht, dass formale Verifikation und Testen komplementäre Starken haben und deshalb kombiniert werden sollten, führte zur Entwicklung eines umfassenden theoretischen Rahmenwerks, welches Verifikation, Testgenerierung, und deduktives Aufdecken von Fehlern in einem zusammenhängenden Ansatz kombiniert. Die Techniken wurden im KeY-System implementiert. Über seine Laufzeit brachte das Projekt vier wichtige Releases von KeY hervor. KeY 1.0 erschien in März 2007 zusammen mit dem Buch „Verification of object-oriented software: The KeY approach“, das laut Google Scholar inzwischen 486 mal zitiert worden ist. KeY 1.6 erschien in Oktober 2010.

Publications

• A dynamic logic for deductive verification of concurrent programs. In Mike Hinchey and Tiziana Margaria, editors, Proceedings, 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), London, UK. IEEE Computer Society, 2007
  Bernhard Beckert and Vladimir Klebanov
  
• Generating unit tests from formal proofs. In Yuri Gurevich and Bertrand Meyer, editors, Proceedings, Tests and Proofs, First International Conference, TAP 2007, Zurich, Switzerland, volume 4454 of LNCS, pages 169–188. Springer, 2007
  Christian Engel and Reiner Hähnle
  
• The KeY System 1.0 (deduction component). In Frank Pfenning, editor, Proceedings, 21st International Conference on Automated Deduction (CADE-21), LNCS 4603, pages 379–384. Springer, 2007
  Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt
  
• Verifying the Mondex case study. In Proceedings, 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), London, England, UK, pages 47–58. IEEE Computer Society, 2007
  Peter H. Schmitt and Isabel Tonin
  
• Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer-Verlag, 2007
  Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt, editors
  
• White-box testing by combining deduction-based specification extraction and black-box testing. In B. Meyer and Y. Gurevich, editors, Proceedings, International Conference on Tests and Proofs (TAP), Zurich, Switzerland, LNCS 4454. Springer, 2007
  Bernhard Beckert and Christoph Gladisch
  
• Predicate abstraction in a program logic calculus. In Michael Leuschel and Heike Wehrheim, editors, Proceedings, 7th International Conference on integrated Formal Methods (iFM 2009), LNCS 5423, pages 136–150. Springer, 2009
  Benjamin Weiß
  
• Generating regression unit tests using a combination of verification and capture & replay. In Gordon Fraser and Angelo Gargantini, editors, Tests and Proofs. Fourth International Conference, TAP 2010, Malaga, Spain. Springer, 2010
  Christoph Gladisch, Shmuel Tyszberowicz, Bernhard Beckert, and Amiram Yehudai
  
• Dynamic frames in Java dynamic logic. In Bernhard Beckert and Claude Marché, editors, Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), volume 6528 of LNCS, pages 138–152. Springer, 2011
  Peter H. Schmitt, Mattias Ulbrich, and Benjamin Weiß