The evolving of CASM : modern compiler engineering and empirical guided language design for a rigorous state-based method

Philipp Paulweber

doi:10.25365/thesis.71894

You are here: University of Vienna PHAIDRA Detail o:1415795

Title (eng)

The evolving of CASM

modern compiler engineering and empirical guided language design for a rigorous state-based method

Author

Philipp Paulweber

Advisor

Uwe Zdun

Assessor

Egon Börger

Matthias Tichy

Abstract (deu)

Die Nachfrage nach der Anwendung formaler Methoden im Bereich der Software-, Hardware- und System-Entwicklung ist nach wie vor ungebrochen. In den letzten Jahrzehnten wurden mehrere domänenspezifische Sprachen (DSLs) und Werkzeuge entwickelt, um verschiedene Arten von Entwurfsherausforderungen zu bewältigen, Anforderungen zu erfassen und geeignete Entwicklungsunterstützung durch Codegenerierungstechniken für Software- und Hardwarebereiche anzubieten. Trotz der intensiven Untersuchung und Erforschung der jeweiligen Domäne fehlt es den meisten Entwicklungsmethoden an geeigneten Techniken, um über das spezifizierte Design Aussagen zu treffen. An dieser Stelle kommen formale Methoden ins Spiel, die in allen verschiedenen Entwicklungs-Bereichen eine Rolle spielt. Die industrielle Hardware-Entwicklung wird zumeist mit Hilfe formaler Methoden durchgeführt oder unterstützt, während formale Methoden in der Software- und Systementwicklung im Allgemeinen immer noch als eine eher akademische Disziplin angesehen werden, obwohl Forscher in aller Welt bereits große Anstrengungen unternommen haben. Insbesondere im Softwarebereich werden sie für die Industrie immer relevanter, da fehlerhaftes Verhalten, Sicherheitsmängel, Sicherheitsverletzungen usw. den Ruf und den Marktanteil eines Unternehmens beeinträchtigen oder bei sicherheitskritischen oder eingebetteten Anwendungen sogar Menschenleben kosten können. Infolgedessen wurden Methoden des modellgetriebene Systementwicklung (MDSE) entwickelt, die umfangreiche Techniken der modellbasierten Entwicklung (MDD) für einen bestimmten Entwicklungsbereich bieten. Die MDD-Technik umfasst eine DSL und ein Werkzeug, das aus einem speziellen Parser, einem Sprachvalidierungsanalysator und einem Codegenerator besteht. Leider sind fast alle MDSE-Methoden maßgeschneiderte Formalismen für eine bestimmte Problemdomäne. Einige dieser Techniken definieren und beschreiben die Sprachsemantik durch den Codegenerierungsprozess, andere ermöglichen die vollständige oder teilweise Simulation der Systemeigenschaften des spezifizierten Entwurfs vor der Erstellung des eigentlichen Systems. Darüber hinaus kann ein in einer DSL beschriebener Entwurf nicht wiederverwendet oder durch Umschreiben in eine andere DSL übertragen werden, da die Spezifikationssprachen auf einem völlig anderen domänenspezifischen Abstraktionsniveau sich befinden. Die abstrakte Zustandsmaschinen (ASM) Methode ist eine zustandsbasierte formale Methode, die genau als das fehlende Teil in dem oben beschriebenen Spezifikationsdilemma angesehen werden kann. Sie bietet eine domänenunabhängige Möglichkeit, das Verhalten eines Systems zu erfassen, unabhängig davon, ob das spezifizierte System ein Software-, Hardware- oder sogar ein gemischtes Software-/Hardware-System ist. Basierend auf einer ASM Spezifikation können Aussagen getroffen werden, um bestimmte Systemeigenschaften zu überprüfen oder sogar bestimmte Aspekte des beschriebenen Systems wie Sicherheitseinschränkungen zu beweisen. Erwähnenswert ist, dass ASM Spezifikationen standardmäßig ausführbare Spezifikationen sind, was bedeutet, dass jedes ASM spezifizierte System simuliert werden kann, ohne dass eine konkrete Implementierung erstellt oder abgeleitet werden muss. Letztere kann per Definition entweder durch Verfeinerungstechniken oder durch Codegenerierung abgeleitet werden, wie dies bei MDSE/MDD der Fall ist. Dennoch mangelt es der Tool-Unterstützung für ASM-basierte Spezifikationssprachen in Bezug auf die Interpretation (Simulation) und Codegenerierung an modernen Compilertechniken und aktuellen Sprachkonzepten. Vor einem Jahrzehnt begann ein Forschungsprojekt, das sich mit beiden Problemen - Interpretation und Codegenerierung - befasste und vom Autor durch eine Open-Source Reimplementierung namens Corinthian Abstract State Machine (CASM) veröffentlicht wurde. Diese Dissertation beschreibt die inkrementell abgeleitete ASM-basierte Compiler-Grundlage und das Framework für CASM, um weitere (optimierte) Compiler- und Interpreter-Potenziale zu erforschen und zu untersuchen sowie die Möglichkeit zu geben, neue Sprachdesignkonzepte zu erforschen. Im Rahmen dieser Arbeit wurde ein neuartiges ASM-basiertes modellbasiertes Transformationsframework unter Verwendung eines Compiler mit mehrstufigen Zwischendarstellungen (IR) erarbeitet, um eine flexible Software- und/oder Hardwarecodegenerierung mit Optimierungsfokus im Vordergrund sowie eine schnelle Ausführung (Interpretation/Simulation) als zweites großes Forschungsziel zu erreichen. Die definierte ASM-basierte IR erlaubt es, ASM-bezogene Compileroptimierungen durch ein klar definiertes Modell zu erforschen und zu definieren und eine einheitliche Schnittstelle für andere ASM-basierte Sprachen- und Werkzeugentwickler bereitzustellen, um z.B. die Implementierung in CASM wiederzuverwenden. Darüber hinaus wurde in dieser Arbeit auch eine verbesserte symbolische Ausführung für CASM entwicklet, die auf der ASM-basierten IR umgesetzt wurde. Diese Dissertation berichtet über die Untersuchung und Einführung eines objekt-orientierten Sprachkonstrukts für ASM-basierte Sprachen, das in einem inkrementellen Prozess durch zwei kontrollierte Experimente und von einer Eye-Tracking Studie abgeleitet wurde. Das erste kontrollierte Experiment verglich die Verständlichkeit von drei objektorientierten Abstraktionen, die in einer ASM-basierten Sprache eingeführt wurden, nämlich Interfaces, Mixins und Traits. Die Ergebnisse zeigten, dass Interfaces und Traits ähnlich gut verstanden werden, was zu einem weiteren kontrollierten Experiment führte, in dem die Benutzerfreundlichkeit der beiden objektorientierten Sprachkonstrukte Interfaces und Traits im Kontext einer ASM-basierten Sprachsyntaxerweiterung untersucht wurde. Dabei wurde ein signifikanter Unterschied festgestellt, nämlich dass das Traits-Sprachkonstrukt im Vergleich zum Interfaces-Sprachkonstrukt besser nutzbar ist. Basierend auf dieser Erkenntnis führten wir ein weiteres kontrolliertes Experiment in Form eines Eye-Tracking Experiments für das Trait-basierte Sprachkonstrukt durch, um durch die Analyse der Blickbewegungsmuster sowie des Fixationsverhaltens der Augen Erkenntnisse über die Verständlichkeit der Syntaxerweiterung zu gewinnen. Das Ergebnis der durchgeführten Studien manifestiert sich in einem neuartigen Trait-basierten objektorientierten Sprachkonstrukt in CASM, das ASM-basierten Sprachen nun sogar die Möglichkeit bietet vorhandene und neue ASM Spracheigenschaften einfach in der ASM Sprache selbst zu beschreiben.

Abstract (eng)

The demand for applying rigorous methods in the field of software engineering, hardware engineering, and systems engineering is still as high as ever. Over the last decades, several Domain-Specific Languages (DSLs) and tools were created to tackle different kinds of design challenges, capturing of requirements, and providing proper development support through code generation techniques for software as well as hardware fields. Despite the intensive investigation and domain exploration in their respective fields, most of the engineering methods lack proper techniques to reason about the specified design. This is where formal methods come into the picture of all engineering fields. Industrial hardware engineering and development is mostly done or supported by formal method-based techniques, whereas in software and system engineering in general formal methods are still seen as a more academic discipline despite the effort already achieved by researchers all other the world. Especially for the software domain it becomes more and more relevant to industry because incorrect behavior, safety flaws, security breaches etc. can impact a company’s reputation and market share or it can even cost human lives in safety critical or embedded applications. As a result, Model-Driven System Engineering (MDSE) methods were created which provide rich Model-Driven Development (MDD) techniques for a specific engineering domain. The MDD technique includes a DSL and tool which consists of a dedicated parser, language validation analyzer, and code generator. Unfortunately, almost all MDSE methods are tailor-made formalisms to deal with a specific problem domain. Some of these techniques define and describe the language semantics through the code generation process, others allow for full or partially simulated systems’ properties of the specified design before the creation of the actual system. Furthermore, a described design in one DSL cannot be reused or easily moved through rewriting into another DSL because of the completely different domain-specific abstraction level of the specification languages. The Abstract State Machine (ASM) method is a state-based formal method which can be seen exactly as the missing piece in the described puzzle or specification dilemma above. It supports a domain independent way to capture a system’s behavior regardless of whether the specified system is a software, hardware, or even a mixed software/hardware system. Based on an ASM, specified system reasoning can be applied in order to check certain system properties or even proof certain aspects of the described system like safety constraints. Notable to mention is that ASM specifications are by default executable specifications, which means that any ASM-specified system can be simulated without even creating or deriving a concrete implementation. By definition, the latter can be derived either by refinement techniques or if supported through code generation just like MDSE/MDD does. Nevertheless, the tooling support for ASM-based specification languages regarding the interpretation (simulation) and compilation (code generation) lack modern compiler techniques and state-of-the-art language engineering. A decade ago, a research project started to address both issues – interpretation and compilation – and was made public by the author through an open-source reimplementation named Corinthian Abstract State Machine (CASM). This PhD thesis describes the incrementally derived ASM-based compiler foundation and framework for CASM in order to research and explore further (optimizing) compiler and interpreter potentials as well as give the ability to research new language design concepts. In the course of this work, a novel ASM-based model-based transformation framework was elaborated by using a multi-level Intermediate Representation (IR) compiler design in order to achieve flexible software and/or hardware code generation with optimization focus in the foreground as well as fast execution (interpretation/simulation) as a second major research target. The defined ASM-based IR allows exploring and defining ASM-related compiler optimizations through a well-defined model and to provide a unified interface for other ASM-based language engineers and tool developers to e.g. reuse the implementation in CASM. Furthermore, an improved symbolic execution effort was achieved in this thesis for CASM as well, which is based in the ASM-based IR. This PhD thesis reports on the investigation and introduction of an object-oriented language construct for ASM-based languages, which was derived in an incremental process applying two controlled experiments and one eye-tracking study. The first controlled experiment compared the understandability of three object-oriented abstractions introduced in an ASM-based language namely interfaces, mixins, and traits. Results showed that interfaces and traits have a similar good understanding, which lead to a follow-up controlled experiment investigating the usability of the two object-oriented language constructs interfaces and traits in the context of an ASM-based language syntax extension. A significant difference was discovered in the results, namely that the traits language construct is more usable compared to the interfaces language construct. Based on this insight, we conducted another controlled experiment in the form of an eye-tracking experiment for the trait-based language construct to obtain knowledge about the comprehensability of the syntax extension by analyzing the eye-gaze patterns as well as the eye fixation behavior. The outcome of these conducted studies is manifested in a novel trait-based object-oriented language construct in CASM, which provides an ability for ASM-based languages to easily describe ASM language properties in the language itself.

Keywords (deu)

Abstrakte ZustandsmaschineASMCompilerSprachendesignExperimente

Keywords (eng)

Abstract State MachineASMCompilerLanguage DesignExperiments

Subject (deu)

Software engineering

Subject (deu)

Programmiersprachen

Subject (deu)

Theoretische Informatik

Type (deu)

Dissertation