| Dienstag, 26. Februar 2013 |
Veranstaltungsort: Kármán-Auditorium, Foyer
Veranstaltungsort: Kármán-Auditorium, Hörsaal SFo4
Abstract:
Termination is a crucial property of programs. Therefore,
techniques to analyze termination automatically are highly
important for program verification. Traditionally, techniques for
automated termination analysis were mainly studied for
declarative programming paradigms such as logic programming and
term rewriting. However, in the last years, several powerful
techniques and tools have been developed which analyze the
termination of programs in many programming languages including
Java, C, Haskell, and Prolog.
In order to re-use the wealth
of existing tools and techniques developed for termination
analysis of term rewriting (see e.g., [GTSKF06, Zan03]), we
developed a transformational methodology to prove termination of
programs in different languages. In a front end, the program is
automatically transformed into a term rewrite system (TRS) such
that termination of the TRS implies termination of the original
program. To obtain TRSs which are suitable for automated
termination proofs, the front end proceeds in two steps. In the
first step, the program is executed symbolically to generate a
so-called termination graph. This graph represents all possible
evaluations of the program in a finite way. In the second step,
the edges of the graph are transformed to rewrite rules. Finally,
existing rewriting techniques are used in the back end to prove
termination of the resulting TRS.
We developed such approaches
to prove termination of Prolog [GSSK+12, SKGS+10], Haskell
[GRSK+11], and Java [BMOG12, BOG11, BOvG10, BSOG12, OBvG10]), and
integrated them into our termination tool AProVE [GST06]. As
shown at the annual International Termination Competition,1
AProVE is currently not only the most powerful tool for automated
termination analysis of TRSs, but also for Prolog, Haskell, and
Java. This shows that the proposed methodology for rewrite-based
automated termination analysis indeed leads to competitive
results.
1See http://termination-portal.org/wiki/Termination_Competition
Abstract: We report on a case study of implementing parallel variants of the Davis-Putnam-Logemann-Loveland algorithm for solving the SAT problem of propositional formulas in the functional programming language Haskell. We explore several state of the art programming techniques for parallel and concurrent programming in Haskell and provide the corresponding implementations. Based on our experimental results, we compare several approaches and implementations.
Abstract:
The Python programming language supports object-oriented
programming using a simple and elegant model that treats member
variables, methods, and various metadata as instances of a single
kind of 'attribute'. While this allows a simple implementation of
an interpreter that supports advanced metaprogramming features,
it can inhibit the performance of certain very common special
cases. This paper deals with the optimization of code that loads
and then calls object methods.
We modify Python's compiler to
emit special bytecode sequences for load/call pairs on object
attributes to avoid unnecessary allocation of method
objects. This can result in considerable speedups, but may cause
slowdowns at call sites that refer to builtin functions or other
special attributes rather than methods. We therefore extend this
static compile-time approach by a dynamic runtime quickening
scheme that falls back to the generic load/call sequence at such
call sites.
The experimental evaluation of dynamic unboxing
shows speedups of up to 8% and rare slowdowns caused by as yet
unresolved excessive instruction cache misses. A comparison with
a common manual optimization of method calls in Python programs
shows that our automatic method is not as powerful but more
widely applicable.
Abstract: Simulation of processors is needed in early stages of development to reduce cost and increase quality of processor designs. Suitable simulators can be generated automatically from high-level specifications of the processor architecture. For this purpose, we have developed the domain specific visual language ViCE-UPSLA. It allows to describe pipeline based register-register, register-memory processor architectures and generates efficient simulators for such processors. In this way a variety of processors can be quickly prototyped for validation and evaluation. We have successfully used ViCE-UPSLA to model and simulate a processor with an ARM [ARM00] like architecture.
Abstract: In this paper we present CASM, a general purpose programming language based on abstract state machines (ASMs). We describe the implementation of an interpreter and a compiler for the language. The demand for efficient execution forced us to modify the definition of ASM and we discuss the impact of those changes. A novel feature for ASM based languages is symbolic execution, which we briefly describe. CASM is used for instruction set simulator generation and for semantic description in a compiler verification project. We report on the experience of using the language in those two projects. Finally we position ASM based programming languages as an elegant combination of imperative and functional programming paradigms which may liberate us from the von Neumann style as demanded by John Backus.
Abstract: Entwickler mobiler Anwendungen, sogenannter Apps, stehen einer heterogenen Landschaft an mobilen Plattformen gegenüber, die sich hinsichtlich ihrer Programmierung stark unterscheiden. Häufig sollen zumindest die weit verbreiteten Betriebssysteme iOS und Android unterstützt werden. Dabei sollen Apps dem nativen, plattformtypischen Aussehen und Verhalten genügen oder zumindest nachempfunden werden. Bestehende Cross-Plattform-Lösungen im mobilen Umfeld unterstützen letztere Anforderung nicht, so dass Entwickler oftmals gezwungen sind, dieselbe App parallel für mehrere Plattformen nativ zu entwickeln. Dies erhöht den Entwicklungsaufwand erheblich, zumal die Implementierung auf einem niedrigen Abstraktionsniveau erfolgt. Dieser Beitrag stellt das Framework MD2 und die domänenspezifische Sprache MD2-DSL vor, die es ermöglicht, Apps mit vorwiegend geschäftlichem Hintergrund auf einem gehobenen Abstraktionsniveau prägnant zu beschreiben. Der modellgetriebene Ansatz MD2 generiert aus den textuellen MD2-DSL-Modellen iOS- und Android-Apps. Die Sprache MD2-DSL enthält Konstrukte zur Abbildung und Umsetzung typischer Anforderungen an Apps und stellt somit eine Alternative zur wiederholten Implementierung einer App auf verschiedenen Plattformen dar.
Abstract:
The Android operating system is currently dominating the mobile
device market in terms of penetration and growth rate. An
important contributor to its success are a wealth of cheap and
easy-to-install mobile applications, known as apps. Today,
installing untrusted apps is the norm, though this comes with
risks: malware is ubiquitous and can easily leak confidential and
sensitive data.
In this work, we investigate
the extent to which we can specify complex information flow
properties using existing specification languages for runtime
monitoring, with the goal to encapsulate potentially harmful apps
and prevent private data from leaking. By modelling a set of
representative, Android-specific security policies with
Tracematches, JavaMOP, Dataflow Pointcuts and PQL, we are able to
identify policylanguage features that are crucial for effectively
defining runtime-enforceable Android security properties.
Our evaluation demonstrates
that while certain property languages suit our purposes better
than others, they all lack essential features that would, if
present, allow users to provide effective security guarantees
about apps. We discuss those shortcomings and propose several
possible mechanisms to overcome them.
Abstract: We present the JOANA (Java Object-sensitive ANAlysis) framework for information flow control (IFC) of Java programs. JOANA can analyze a given Java program and guarantee the absence of security leaks, e.g. that a online banking application does not send sensitive information to third parties. It applies a wide range of program analysis techniques such as dependence graph computation, slicing and chopping of sequential as well as concurrent programs. We introduce the Java Web Start application IFC Console and show how it can be used to apply JOANA to arbitrary programs in order to specify and verify security properties.
Abstract: Model-driven software development employs models to describe different aspects of a system on different levels of abstraction. These aspects are driven by technology or application domain. Modeling is often done in specific graphical or textual notations, called domain-specific languages (DSL). In recent years such languages became very popular in the modeling community to describe structure and sometimes behavior. In the context of type systems, these structures are called types and the behavior is modeled with expressions. The programming language community has developed many concepts to model and specify type systems and the semantics of expressions. However, in the modeling community this is often neglected when specifying meta models and describing their semantics, what may cause problems in developing checks and generators for DSLs. To address this issue, we present an approach, that provides guidance and support during DSL development based on established knowledge on type systems and generator construction, to ease the integration of type systems in DSL. We evaluate this approach with the Xtext language engineering framework.
Abstract:
Software development for Cyber-Physical Systems (CPS) is a
sophisticated activity as these systems are inherently
complex. The engineering of CPS requires composition and
interaction of diverse distributed software modules. Describing
both, a system~s architecture and behavior in integrated models,
yields many advantages to cope with this complexity: the models
are platform independent, can be decomposed to be developed
independently by experts of the respective fields, are highly
reusable and may be subjected to formal analysis.
In this paper,
we introduce a code generation framework for the
MontiArcAutomaton modeling language. CPS are modeled as Component
& Connector architectures with embedded I/Oω automata. During
development, these models can be analyzed using formal methods,
graphically edited, and deployed to various platforms. For this,
we present four code generators based on the MontiCore code
generation framework, that implement the transformation from
MontiArcAutomaton models to Mona (formal analysis), EMF Ecore
(graphical editing), and Java and Python (deployment). Based on
these prototypes, we discuss their commonalities and differences
as well as language and application specific challenges focusing
on code generator development.
Abstract: Professional development of software dealing with structured models requires more systematic approach and semantic foundation than standard practice in general-purpose programming languages affords. One remedy is to integrate techniques from other programming paradigms, as seamless as possible and without forcing programmers to leave their comfort zone. Here we present a tool for the implementation of pattern matching as fundamental means of automated data extraction from models of arbitrary shape and complexity in a general-purpose programming language. The interface is simple but, thanks to elaborate and rigorous design, is also light-weight, portable, non-invasive, type-safe, modular and extensible. It is compatible with object-oriented data abstraction and has full support for nondeterminism by backtracking. The tool comes as a library consisting of two levels: elementary pattern algebra (generic, highly reusable) and pattern bindings for particular data models (specific, fairly reusable, user-definable). Applications use the library code in a small number of idiomatic ways, making pattern-matching code declarative in style, easily writable, readable and maintainable. Library and idiom together form a tightly embedded domain-specific language; no extension of the host language is required. The current implementation is in Java, but assumes only standard object-oriented features, and can hence be ported to other mainstream languages.
Abstract:
In der vergangenen Dekade hat Modell-basierte Entwicklung in der
Softwaretechnik zunehmende Bedeutung gewonnen, vgl. z.B. [TS07,
SRC+ 12, JLM+ 12]. Aus Modellen, die in einer formalen Sprache
definiert sind (Domänen-spezifische Sprache) wird Code
generiert, der die Modelle implementiert. Da Domänen-spezifische
Sprachen nicht selten starken Änderungen und Erweiterungen
unterworfen sind, haben sich Werkzeugkästen wie beispielsweise
das Eclipse Modeling Framework (kurz: EMF) etabliert [SBMP08],
mit deren Hilfe die Codegeneratoren selbst generiert werden
können. Zur Spezifikation Domänen-spezifischer Sprachen wird ein
Metamodell definiert, aus dem dann mittels
Modelltransformationen die Transformationsregeln in die
Zielsprache spezifiziert werden. Neben dem Codegenerator für
eine Domänen-spezifische Sprache werden beispielsweise mit der
EMF-Technologie Editoren für die Domänen-spezifische Sprache
generiert, die auch durch die Eclipse-Technologie in
Programmier- und Anwendungsumgebungen eingebettet werden können.
Als grundlegende Technologie werden Metamodelle meist in
graphischer Form (z.B. UML-Klassendiagrammen) oder durch eine
kontextfreie Grammatik [EEK+ 12] definiert. Mittels OCL können
Konsistenzbedingungen angegeben werden, die alle Modelle einer
Domänen-spezifischen Sprache erfüllen müssen. Meist führen diese
zu Laufzeitprüfungen. Oft werden zusätzlich im Code des
Modell-basierten Codegenerators noch manuelle Ergänzungen und
Änderungen vorgenommen. Gründe können Effizienzsteigerungen in
der Codegenerierung oder weitere Überprüfungen sein. Eine
Weiterentwicklung einer Domänen-spezifischen Sprache erfordert
daher nicht selten eine grundsätzliche Revision und
Überarbeitung des Codegenerators.
Die Aufgabenstellung für
Übersetzer ist nahezu identisch: ein Programm in höherer
Programmiersprache wird in ein Programm einer Maschinensprache
oder einer anderen Hochsprache (Cross-Compiler) transformiert. In
einem Übersetzer wird der Quelltext auf korrekte Syntax hin
analysiert und in eine interne Datenstruktur, den abstrakten
Syntaxbaum transformiert. Anschließend werden
Konsistenzbedingungen wie beispielsweise Typkorrektheit
analysiert. Im Falle eines Cross-Compilers wird der abstrakte
Syntaxbaum in das Zielprogramm transformiert, ansonsten in eine
Zwischensprache, die weiter in den Maschinencode übersetzt
wird. Hier haben sich z.T. seit Mitte der 1970er Jahre Werkzeuge
[Joh75, KHZ82, DUP+82] und Werkzeugkästen zur Generierung von
Übersetzern etabliert. Aktuelle Werkzeugkästen sind
beispielsweise ANTLRv3 [Par07] oder Eli [KWS07]. Die
Syntaxanalyse wird durch Angabe der Lexik als reguläre Ausdrücke,
durch eine kontextfreie Grammatik für die konkrete Syntax und der
Datenstruktur für die abstrakte Syntax angegeben. Die
Konsistenzprüfungen können aus geordneten Attributierten
Grammatiken generiert werden, die Transformation in die
Zielsprache bzw. Zwischensprache wird aus Baumtransformationen
generiert. Im generierten Übersetzer müssen keine Änderungen mehr
vorgenommen werden, da Hilfsfunktionen Bestandteil der
Spezifikationen sind. Hilfsfunktionen sind bereits in der
Wirtssprache (der Sprache, in der der Übersetzer implementiert
ist) definiert. Sie können deshalb problemlos eingebunden und
geändert werden. Dadurch ist es nicht notwendig, den generierten
Code anzufassen, und man kann agil einen Übersetzer Sprachkonzept
um Sprachkonzept anreichern.
Als Fazit ergibt sich eine
deutliche Korrespondenz zwischen der Generierung Modellbasierter
Codegeneratoren und der Generierung von Übersetzern (vgl. auch
[Jör11]): Die Begriffe Metamodell und Abstrakte Syntax sind
konzeptuell identisch. Konsistenzbedingungen werden durch
unterschiedliche Technologien wie OCL bzw. attributierte
Grammatiken definiert und Modelltransformationen entsprechen
konzeptuell Baumtransformationen. Für die praktische Entwicklung
von Modell-basierten Codegeneratoren kann daher ohne Weiteres
Übersetzerbautechnologie verwendet werden. Ein möglicher Vorteil
durch die Verwendung von attributierten Grammatiken an Stelle von
OCL wäre eine statische Prüfung der Konsistenz der Modelle
anstatt dies auf Laufzeitprüfungen zu verlagern. Durch die
Definition von Hilfsfunktionen in der Wirtssprache anstelle derer
nachträglichen manuellen Integration in den Codegenerator wäre
eine agilere und kostengünstigere Entwicklung von
Modell-basierten Codegeneratoren möglich. Die für die
industrielle Praxis wichtige Generierung der Editoren für
Domänen-spezifische Sprachen und deren Einbettung in Programmier-
und Anwendungsumgebungen müsste allerdings noch erfolgen, da dies
durch Übersetzertechnologie bisher wenig Beachtung gefunden hat.
