TU Darmstadt / ULB / TUprints

Integrating Symbolic Execution, Debugging and Verification

Hentschel, Martin :
Integrating Symbolic Execution, Debugging and Verification.
Technische Universität Darmstadt
[Ph.D. Thesis], (2016)

[img]
Preview
Text
PhD_thesis.pdf
Available under Creative Commons Attribution Non-commercial No-derivatives 3.0 de.

Download (6MB) | Preview
Item Type: Ph.D. Thesis
Title: Integrating Symbolic Execution, Debugging and Verification
Language: English
Abstract:

In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management.

Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect.

This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well.

In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment.

Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY.

The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY.

Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods.

Alternative Abstract:
Alternative AbstractLanguage
Eine integrierte Entwicklungsumgebung (IDE) unterstützt nahezu alle Aspekte moderner Softwareentwicklung. Neben den klassischen Anwendungsfällen wie das Schreiben, Ausführen und Debuggen von Quellcode, fungiert sie auch als Schnittstelle zu allen anderen Werkzeugen, die im Entwicklungsprozess eingebunden sind. Dies sind z. B. Versionsverwaltungs- oder Anwendungsmanagementsysteme. Unabhängig vom verwendeten Entwicklungsprozess sind die Techniken, um fehlerfreie Software zu entwickeln, immer die gleichen. Das Ziel ist es Fehler so früh wie möglich zu finden, denn je eher ein Fehler gefunden wird, desto einfacher und günstiger ist er zu beheben. An erster Stelle verhindern Programmiersprachen gewisse Arten von Fehlern. Sobald etwas geschrieben wurde, ist ein Review ein effektives Werkzeug, um Fehler zu finden und die Qualität zu erhöhen. Eine statische Analyse kann gewisse Fehler ebenfalls automatisch finden. Das ausgewählte Szenarien richtig funktionieren, wird durch Tests sichergestellt. Ein Test kann jedoch nur die Gegenwart und nicht die Abwesenheit eines Fehlers zeigen. Um sicherzustellen, dass ein Programm richtig ist, muss gezeigt werden, dass es einer formalen Spezifikation, welche das gewünschte Verhalten beschreibt, entspricht. Dies wird mittels formaler Verifikation erreicht. Sobald ein Fehler gefunden wurde, muss dessen Ursache schließlich durch Debuggen gefunden werden. Diese Arbeit erweitert das Softwareentwicklungs-Portfolio um einen interaktiven Debugger basierend auf symbolischer Programmausführung, eine Technik die alle möglichen Programmausführungspfade bis zu einer gegebenen Tiefe zeitgleich erkundet. Der resultierende Debugger kann nicht nur für klassische Debugging-Aktivitäten verwendet werden, sondern auch für Reviews oder um Ergebnisse einer Analyse basierend auf symbolischer Programmausführung darzustellen. Im Rahmen dieser Arbeit wird die symbolische Programmausführung erweitert, um das gesamte Programmverhalten auch in Gegenwart von Schleifen und rekursiven Methodenaufrufen zu erkunden. Dies wird durch die Integration von Spezifikationen in Form von Schleifeninvarianten und Methodenverträgen erreicht. Ebenfalls wird gezeigt, wie solch eine symbolische Ausführungseinheit basierend auf Verifikations-Beweisen realisiert werden kann. Zusätzlich wird der Symbolic Execution Debugger (SED) vorgestellt, welcher die Eclipse Plattform für Debugger basierend auf symbolischer Programmausführung vorbereitet. Die Funktionalität geht dabei über die traditioneller Debugger hinaus, z. B. kann das Debuggen direkt bei jeder beliebigen Methode oder Anweisung beginnen. Ebenso werden alle möglichen Programmausführungspfade zeitgleich erkundet. Um das Programmverstehen zu erhöhen, werden Ausführungspfade und Zustände visualisiert. Standardmäßig stellt der SED eine symbolische Ausführungseinheit basierend auf dem Verifikationssystem KeY zur Verfügung. Ein statistischer Nachweis, dass der SED die Effektivität von Reviews erhöht, wird durch ein kontrolliertes Experiment erbracht. Eine weitere Neuheit des SED ist, das beliebige Verifikationsbeweise inspiziert werden können. Während traditionelle Benutzeroberflächen von Verifikationswerkzeugen einen Beweis aus mathematischer Sicht präsentieren, analysiert der SED den gesamten Beweis und präsentiert unterschiedliche Aspekte mittels verschiedener Sichten. Ein kontrolliertes Experiment weist durch einen Vergleich mit der originalen Benutzeroberfläche von KeY nach, dass das Beweisverstehen durch den SED erhöht wird. Der SED ermöglicht mit dem darunterliegenden Beweiser durch Anpassung des Quellcodes und dessen Spezifikationen zu interagieren. Dies schafft das Bedürfnis, Beweise direkt innerhalb der IDE zu verwalten. Dazu wird ein Konzept präsentiert, welches ein semi-automatisches Verifikationswerkzeug in eine IDE integriert. Es beinhaltet mehrere Optimierungen, um die Zeit der Beweisführung zu reduzieren. Zusätzlich kann es ohne Anpassung des Verifikationswerkzeugs realisiert werden. Eine optimale Benutzererfahrung wird jedoch nur erreicht, wenn alle Aspekte der Verifikation direkt von der IDE unterstützt werden. Deshalb wird eine vollständige Integration von KeY in Eclipse vorgestellt, welche beispielsweise zusätzlich zum Beweismanagement auch das Schreiben von JML-Spezifikationen und das Bereitstellen der benötigten Infrastruktur zum Beweisen mit KeY unterstützt. Insgesamt wird eine Plattform für Werkzeuge basierend auf symbolischer Programmausführung und verwandt zur Verifikation vorgestellt, welche eine nahtlose Integration in eine IDE und eine gemeinsame Nutzung fördert. Viele Aspekte, wie z. B. die Art wie Beweise im SED dem Benutzer dargestellt werden, helfen die Barrieren beim Einsatz formaler Methoden zu reduzieren.German
Uncontrolled Keywords: Symbolic Execution, Debugging, Program Execution Visualization, Verification, Proof Understanding, Code Review, Empirical Evaluation, Integration of Formal Methods into Software Engineering Practice
Alternative keywords:
Alternative keywordsLanguage
Symbolische Programmausführung, Debugging, Visualisierung von Programmausführungen, Verifikation, Beweisverstehen, Quellcode Review, Empirische Evaluation, Integration von formalen Methoden in die Software Engineering PraxisGerman
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: 20 Department of Computer Science
Date Deposited: 10 May 2016 12:57
Last Modified: 10 May 2016 12:57
URN: urn:nbn:de:tuda-tuprints-53995
Referees: Hähnle, Prof. Dr. Reiner and Leino, Prof. Dr. K. Rustan M.
Refereed: 8 March 2016
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/5399
Export:
Actions (login required)
View Item View Item

Downloads

Downloads per month over past year