Detailansicht
New Symbolic Execution Pass for the CASM language
Jakob Moosbrugger
Art der Arbeit
Masterarbeit
Universität
Universität Wien
Fakultät
Fakultät für Informatik
Studiumsbezeichnung bzw. Universitätlehrgang (ULG)
Masterstudium Informatik
Betreuer*in
Uwe Zdun
DOI
10.25365/thesis.65668
URN
urn:nbn:at:at-ubw:1-21282.26194.963766-3
Link zu u:search
(Print-Exemplar eventuell in Bibliothek verfügbar)
Abstracts
Abstract
(Deutsch)
Heutzutage ist es wichtig, dass Software korrekt arbeitet, da sie oft auch in sicherheit-
skritischen Bereichen verwendet wird. Eine Methode zur Beschreibung von Software sind
Abstract State Machines (ASM). ASMs sind eine Erweiterung von Finite State Machines
(FSM) und sind formal definiert. Da sie auf mathematischen Grundlagen basieren, ist es
möglich, bestimmte Eigenschaften mittels formalen Methoden zu beweisen. Es müssen
jedoch nicht nur die modellierten Systeme fehlerfrei sein, sondern auch die Compiler, welche
verwendet werden, um die abstrakte Repräsentation in eine ausführbare Datei zu überset-
zen. Diese dürfen keine Fehler einbringen. Translation Validation ist eine Möglichkeit zu
zeigen, dass ein bestimmter Compilier-Vorgang fehlerfrei ist. Für Translation Validation
wird ein mathematisches Modell der Input Spezifikation und des Outputs erstellt und
gezeigt, dass die Modelle ident sind.
Diese Arbeit ist der erste Schritt in Richtung Translation Validation im Corinthian
Abstract State Machine (CASM) Compiler, indem es ein Framework präsentiert, welches
eine in CASM geschriebene ASM in ihre Repräsentation in der TPTP Sprache übersetzt.
Die Arbeit basiert auf einem von Lezuo [48] vorgestellten Ansatz. Die TPTP Sprache ist
als Input für Automated Theorem Prover (ATP) Systeme entworfen. Die Transformation
unterstützt concolic execution. Um sicherzustellen, dass dabei numerische Funktionen nicht
symbolischen Werten zugewiesen werden, wird in dieser Arbeit ein neues System vorgestellt,
welches vor der Transformation das Auftreten solcher Zuweisungen prüft. Falls derartige
Zuweisungen existieren, wird die entsprechende Funktion von numerisch zu symbolisch
umgewandelt. Außerdem wird eine direkte Transformation von TPTP zu einem Model für
den Satisfiablity Modulus Theories (SMT) Solver Z3 vorgestellt.
Abstract
(Englisch)
Nowadays it is important that software works correctly as it is often used in safety-critical
systems. One method for describing systems on a high level are Abstract State Machines
(ASM). ASMs are an extension of Finite State Machines and are formally defined. As
they are based on mathematical foundations, it is possible to prove certain properties of
an ASM using formal methods. However, not only the modeled systems need to be error
free but also compilers which are used to translate the high level representation to an
executable file also must not introduce any errors. Translation Validation is one method to
prove that a specific compilation did not introduce any errors. For translation validation
a mathematical model of the input and the output of the compilation is built and then
proven that they are identical.
This thesis takes the first step towards translation validation in the Corinthian Abstract
State Machine (CASM) compiler, by presenting a framework that transforms an ASM
written in the CASM language into a representation in the TPTP language. It is based on
a previously introduced approach by Lezuo [48]. The TPTP language is designed as input
for Automated Theorem Prover (ATP) systems. The transformation supports concolic
execution. In order to ensure that numeric functions are not updated with symbolic values,
this thesis presents a new system which checks whether such updates occur before the
actual transformation takes place. If such updates occur the system promotes numeric
functions to symbolic functions accordingly. Furthermore, a transformation from the
TPTP model directly to the model of the Satisfiablity Modulus Theories (SMT) solver Z3
is presented.
Schlagwörter
Schlagwörter
(Englisch)
symbolic execution CASM translation validation compiler TPTP
Schlagwörter
(Deutsch)
Symbolic Execution CASM Symbolische Ausführung Translation Validation Compiler TPTP
Autor*innen
Jakob Moosbrugger
Haupttitel (Englisch)
New Symbolic Execution Pass for the CASM language
Paralleltitel (Deutsch)
Neuer Symbolic Execution Pass für die CASM Sprache
Publikationsjahr
2021
Umfangsangabe
xvi, 77 Seiten : Diagramme
Sprache
Englisch
Beurteiler*in
Uwe Zdun
Klassifikationen
54 Informatik > 54.10 Theoretische Informatik ,
54 Informatik > 54.53 Programmiersprachen
AC Nummer
AC16273384
Utheses ID
58166
Studienkennzahl
UA | 066 | 921 | |