The following technical report is available from
http://aib.informatik.rwth-aachen.de:
A Linear Operational Semantics for Termination and Complexity Analysis
of ISO Prolog
Thomas Ströder, Fabian Emmes, Peter Schneider-Kamp, Jürgen Giesl,
Carsten Fuhs
AIB 2011-08
We present a new operational semantics for Prolog which covers all
constructs in the corresponding ISO standard (including "non-logical"
concepts like cuts, meta-programming, "all solution" predicates,
dynamic predicates, and exception handling). In contrast to the
classical operational semantics for logic programming, our semantics
is linear and not based on search trees. This has the advantage that
it is particularly suitable for automated program analyses such as
termination and complexity analysis. We prove that our new semantics
is equivalent to the ISO Prolog semantics, i.e., it computes the same
answer substitutions and the derivations in both semantics have
essentially the same length.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Hierarchical Counterexamples for Discrete-Time Markov Chains
Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer,
Joost-Pieter Katoen, Bernd Becker
AIB 2011-11
In this paper we introduce a novel counterexample generation approach
for discrete-time Markov chains (DTMCs) with two main advantages:
(1) We generate *abstract* counterexamples, which
can be refined in a *hierarchical* manner.
(2) We aim at minimizing the number of states involved in the
counterexamples, and compute a *critical subsystem* of the DTMC,
whose paths form a counterexample.
Experiments show that with our approach we can reduce the size of
counterexamples and the number of computation steps by orders of
magnitude.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
A Dependency Pair Framework for Innermost Complexity Analysis
of Term Rewrite Systems
Lars Noschinski, Fabian Emmes, Jürgen Giesl
AIB 2011-03
We present a modular framework to analyze the innermost runtime
complexity of term rewrite systems automatically. Our method is
based on the dependency pair framework for termination analysis.
In contrast to previous work, we developed a direct adaptation
of successful termination techniques from the dependency pair
framework in order to use them for complexity analysis. By
extensive experimental results, we demonstrate the power of
our method compared to existing techniques.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Modular Termination Proofs of Recursive Java Bytecode Programs
by Term Rewriting
Marc Brockschmidt, Carsten Otto, Jürgen Giesl
AIB 2011-02
In earlier work we presented an approach to prove termination of
non-recursive Java Bytecode (JBC) programs automatically. Here,
JBC programs are first transformed to finite termination graphs
which represent all possible runs of the program.
Afterwards, the termination graphs are translated to term
rewrite systems (TRSs) such that termination of the resulting TRSs
implies termination of the original JBC programs. So in this way,
existing techniques and tools from term rewriting can be used to
prove termination of JBC automatically. In this paper, we improve
this approach substantially in two ways:
(1) We extend it in order to also analyze recursive JBC programs.
To this end, one has to represent call stacks of arbitrary
size.
(2) To handle JBC programs with several methods, we modularize our
approach in order to re-use termination graphs and TRSs for the
separate methods and to prove termination of the resulting TRS
in a modular way.
We implemented our approach in the tool AProVE. Our experiments show
that the new contributions increase the power of termination analysis
for JBC significantly.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
A Local Greibach Normal Form for Hyperedge Replacement Grammars
Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll
AIB 2011-04
Heap-based data structures play an important role in modern programming
concepts. However standard verification algorithms cannot cope with
infinite state spaces as induced by these structures.
A common approach to solve this problem is to apply abstraction
techniques. Hyperedge replacement grammars provide a promising technique
for heap abstraction as their production rules can be used to partially
abstract and concretise heap structures.
To support the required concretisations, we introduce a normal form for
hyperedge replacement grammars as a generalisation of the Greibach
Normal Form for string grammars and the adapted construction.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Degrees of Lookahead in Context-free Infinite Games
Wladimir Fridman, Christof Löding, Martin Zimmermann
AIB 2010-20
We continue the investigation of delay games, infinite games in which
one player may postpone her moves for some time to obtain a lookahead
on her opponents moves. We show that the problem of determining the
winner of such a game is undecidable for context-free winning
conditions. Furthermore, we show that the necessary lookahead to win a
context-free delay game cannot be bounded by an elementary function.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Experimental Evaluation of an Independent Set Algorithm
Felix Reidl
AIB 2010-19
Following up the development of the currently fastest Independent Set
algorithm (Kneis, Langer, Rossmanith, 2009) we present a practical
evaluation, both on real-world data taken from common biological
problems and on synthetic data. In order to get a clearer picture we
measure different aspects of our implementation, especially the
different polynomial-time reduction rules. The main purpose of this
report is to show that algorithms with provable upper bounds can
indeed be used to solve practical instances, though some care must be
taken in the transfer of algorithm to code.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Personalisierte eHomes: Mobilität, Privatsphäre und Sicherheit
Ibrahim Armaç
AIB 2010-18
eHomes sind intelligente Umgebungen, die ihren Benutzern durch die
Kopplung von Geräte- und Softwarefunktionalitäten einen Mehrwert in
Form von integrierten Diensten bieten. Der Mehrwert besteht darin,
dass den Benutzern neuartige Funktionalitäten angeboten werden, die
sie durch die getrennte Verwendung der einzelnen Geräte nicht erlangen
könnten. Es existiert eine breite Palette von Anwendungsfeldern für
eHome-Dienste wie etwa in den Bereichen Komfort, Sicherheit,
Multimedia, Verbrauchserfassung oder betreutes Wohnen.
Es gibt eine Reihe von Herausforderungen, die für die Entwicklung und
den Betrieb von eHomes überwunden werden müssen. Um die
Interoperabilität der Dienste zu gewährleisten, muss zunächst die aus
der Vielzahl von unterschiedlichen Geräten und Standards resultierende
Heterogenität bewältigt werden. Außerdem muss die hochgradige Dynamik
berücksichtigt werden, um zur Betriebszeit auf Änderungen eingehen zu
können, die sich etwa aus der Mobilität von Geräten und Benutzern
ergeben. Weiterhin sind geeignete Konzepte zur Personalisierung
erforderlich, um Funktionalitäten auf die individuellen Bedürfnisse
der Benutzer anzupassen. Darüber hinaus muss die wechselseitige
Sicherheit von Benutzern und eHomes gewährleistet werden.
Zur Bewältigung der Heterogenitätsherausforderung wurden im Rahmen
eines Forschungsprojekts am Lehrstuhl für Software Engineering (i3) an
der RWTH Aachen bereits Konzepte und Werkzeuge für die Konfigurierung
und den Betrieb von eHomes entwickelt. Hierfür wurde eine
komponentenbasierte Softwarearchitektur entworfen, auf deren Basis
Dienste flexibel und unverändert in mehreren eHomes wiederverwendet
werden können. Die Wiederverwendung wird dabei durch den sogenannten
SCD-Prozess unterstützt, der sich aus den drei Phasen Spezifizierung,
Konfigurierung und Deployment zusammensetzt. In diesem Prozess kann
auf Basis der erfassten Kundenwünsche komfortabel eine
eHome-spezifische Dienstkomposition erstellt und zur Ausführung
gebracht werden. Aufgrund des kontinuierlichen Charakters des
SCD-Prozesses kann die Dienstkomposition im laufenden Betrieb eines
eHomes an Änderungen im Rahmen der erwähnten Dynamik angepasst werden.
Die vorliegende Arbeit ist im Rahmen dieses Projekts entstanden und
betrachtet zwei signifikante Aspekte von eHomes, die in den
Vorgängerarbeiten nicht behandelt wurden.
Die erste Fragestellung betrifft die Unterstützung der
Personalisierung im Rahmen der Inter-eHome-Mobilität, einer speziellen
Art der Dynamik. Hierunter wird der Sachverhalt verstanden, dass
Benutzer häufig zwischen verschiedenen eHomes wechseln. Ziel ist es,
ihre Präferenzen in allen eHomes ohne mehrfachen
Konfigurierungsaufwand soweit wie möglich zu berücksichtigen. Die im
Rahmen dieser Arbeit neu entwickelten Konzepte ermöglichen die
Personalisierung von eHomes auf zwei Arten: Erstens wird ein mobiles
Benutzermodell entwickelt, mit dessen Hilfe die Benutzer ihre
persönlichen Daten eHome-übergreifend auf einem mobilen Gerät
verwalten und den jeweiligen eHomes zur Verfügung stellen können.
Zweitens wird ermöglicht, dass die Benutzer eigene Dienste mitnehmen
und auf ihren mobilen Geräten ausführen. Dadurch können sie gewohnte
Funktionalitäten auch dann nutzen, wenn das besuchte eHome die
Funktionalitäten nicht direkt über einen eigenen Dienst anbietet,
obwohl es über die dafür nötigen Geräte verfügt.
Die zweite Fragestellung bezieht sich auf die Gewährleistung der
wechselseitigen Sicherheit im Rahmen dieser Mobilität. Es werden
sowohl die Schutzziele der Benutzer als auch die der eHomes erfüllt.
Um die Privatsphäre der Benutzer zu schützen, werden Konzepte
entwickelt, die die Einhaltung der Prinzipien Datensparsamkeit und
Unverkettbarkeit persönlicher Daten ermöglichen.
Für die Realisierung der Datensparsamkeit gegenüber eHomes wird ein
aushandlungsbasiertes Identitätsmanagementsystem eingeführt. Mithilfe
dieses Systems können mobile Benutzer sowohl die Menge der einem eHome
preisgegebenen Daten minimieren als auch jedem eHome gegenüber mit
einer anderen Identität entgegentreten. Zur Realisierung der
Datensparsamkeit gegenüber Diensten wird eine selektive
Zugriffskontrolle für die Daten umgesetzt, die einem eHome bereits
offengelegt wurden. Dadurch wird die Menge der einem Dienst zur
Verfügung gestellten Daten auf ein notwendiges Minimum reduziert.
Um eine Verkettbarkeit unterschiedlicher Identitäten durch mehrere
eHomes auszuschließen, wird ein Authentifizierungsmechanismus auf
Basis anonymer Credentials entwickelt. Eine mögliche Verkettbarkeit
der Daten durch mehrere Dienste in einem eHome hingegen wird durch den
Einsatz von Pseudonymen verhindert.
Im Hinblick auf den Schutz von eHome-Diensten vor unbefugten Zugriffen
werden zwei Arten von Zugriffen betrachtet. Für den Schutz vor dem
Zugriff unbefugter Benutzer werden alternative
Zugriffskontrollmechanismen entwickelt, die grob in Credential- und
rollenbasierte Mechanismen unterteilt werden können. Sie erfüllen das
Ziel der Zurechenbarkeit, das die Zuordnung von Aktivitäten zu den
Benutzern ermöglicht, wenn dies erforderlich ist. Für den Schutz vor
unbefugten Zugriffen durch Dienste wird eine rollenbasierte
Zugriffskontrolle eingesetzt. Die Generierung und die dynamische
Anpassung der Zugriffsrechte an eine sich zur Laufzeit ändernde
Dienstkomposition findet dabei vollständig automatisch statt.
Die beschriebenen Konzepte werden in Form neuer Werkzeuge umgesetzt.
Die Anwendbarkeit der Ergebnisse dieser Arbeit wird durch ihre
Evaluierung anhand von Testszenarien gezeigt. Hierfür werden
verschiedene Demonstratoren herangezogen, die im Rahmen dieser Arbeit
entwickelt wurden.
Durch die Ergebnisse dieser Arbeit werden die einander widerstrebenden
Anforderungen Schutz der Privatsphäre und Personalisierung miteinander
in Einklang gebracht. Der entwickelte Lösungsansatz bietet hierfür
einen guten Kompromiss zwischen Anonymität und Zurechenbarkeit.
Insgesamt leistet diese Arbeit einen Beitrag zur Akzeptanz von eHomes,
da mobile Benutzer durch die entwickelten Konzepte von den Vorteilen
personalisierbarer Dienste in unterschiedlichen eHomes profitieren
können, während ihre Privatsphäre geschützt bleibt.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Systemmodell-basierte Definition objektbasierter Modellierungssprachen
mit semantischen Variationspunkten
Hans Grönniger
AIB 2010-17
Eine Voraussetzung für den Erfolg einer modellbasierten Methode zur
Softwareentwicklung ist eine variable und dennoch präzise Definition
der verwendeten Modellierungssprachen. Hierzu gehört insbesondere auch
die explizite Definition der Bedeutung der Sprachen -- ihrer
Semantik. Formale Semantik leistet einen wichtigen Beitrag zur
unmissverständlichen Kommunikation zwischen den Beteiligten und kann
einen hohen Grad der Automatisierung über interoperable Werkzeuge
ermöglichen. Diese Arbeit beschäftigt sich mit der vollständigen,
formalen Definition objektbasierter Modellierungssprachen und legt den
Fokus auf die flexible Definition problemadäquater Semantik.
Zur Definition der Semantik objektbasierter Modellierungssprachen wird
das Systemmodell als von allen Sprachen gemeinsam genutzte semantische
Domäne definiert. Das Systemmodell charakterisiert abstrakt die
Struktur, das Verhalten und die Interaktion von Objekten
objektbasierter Systeme. Die prädikative semantische Abbildung von
Elementen der Syntax einer Sprache in das Systemmodell definiert für
ein Modell eine Menge von objektbasierten Systemen und erzeugt damit
eine präzise Bedeutung auch für unvollständige bzw. unterspezifizierte
Modelle. Die Semantik von Modellkomposition und -verfeinerung kann auf
Basis des Systemmodells durch einfache mathematische Operationen
erklärt werden.
Gemäß einer allgemeinen Klassifikation der möglichen Variabilität
einer Modellierungssprache können die verschiedenen Sprachbestandteile
wie Syntax, semantische Domäne und semantische Abbildung mit Varianten
ausgestattet werden. Dies ermöglicht die Anpassung einer Sprache zum
Beispiel an einen projektspezifischen Kontext. Varianten und ihre
Abhängigkeiten werden in Feature-Diagrammen dokumentiert. Eine
Konfiguration, also die Auswahl von Sprachvarianten gemäß der
Feature-Diagramme, legt dann die Menge der gültigen Definitionen fest.
Die eingeführte Werkzeugunterstützung basiert auf MontiCore, einem
Framework zur modularen Erstellung von textuellen
Modellierungssprachen und dem Theorembeweiser Isabelle/HOL. Hierdurch
wird eine flexible und gleichzeitig maschinenlesbare Syntax und
Semantik gewonnen. Auch die Definition und Konfiguration von
Semantikvarianten wird unterstützt.
Die Definition der Semantik der UML-Teilmenge UML/P dient der
Erprobung des werkzeugunterstützten Vorgehens. Betrachtet werden
Klassendiagrammen, Objektdiagramme, Statecharts und
Sequenzdiagramme. Zudem werden als Aktions- bzw. Constraint-Sprache
vereinfachte Versionen von Java und OCL verwendet.
Die angegebenen Semantikvarianten können direkt zur
maschinenunterstützten Verifikation im Theorembeweiser verwendet
werden, da sich zusätzlich auch konkrete Modelle automatisch in
Isabelle übersetzen lassen. Die Verifikation wird an Beispielen unter
Verwendung integrierter Semantiken verschiedener Modellierungssprachen
der UML/P demonstriert. Dies zeigt die praktische Verwendbarkeit des
Ansatzes.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automating Acceptance Tests for Sensor- and Actuator-based Systems on
the Example of Autonomous Vehicles
Christian Berger
AIB 2010-16
In projects dealing with autonomous vehicles which are driving in
different contexts like highways, urban environments, and rough areas,
managing the software's quality for the entire data processing chain
of sensor- and actuator-based autonomous systems is increasingly
complex. One main reason is the early dependency on all sensor's raw
data to setup the data processing chain and to identify subsystems.
These sensors' data might be extensive, especially if laser scanners
or color camera systems are continuously producing a vast amount of
raw data. Moreover, due to this dependency the sensors' setup
including their respectively specified mounting positions and
calibration information is also necessary to gather real input data
from real surroundings' situations of the system. This is even more
important before actually starting to integrate independently
developed subsystems for carrying out tests for the entire data
processing chain.
To reduce this dependency and therefore to decouple tasks from the
project's critical path, an approach is outlined in this thesis which
was developed to support the software engineering for sensor- and
actuator-based autonomous systems. This approach relies on customer's
requirements and corresponding customer's acceptance criteria as well
as the decoupling of the software engineering from the real hardware
environment to allow appropriate system simulations.
Based on the customer's requirements, formally specified scenarios
using a domain specific language are derived which are used to provide
surroundings and suitable situations for a sensor- and actuator-based
autonomous system. From these formally specified surroundings, the
required input data is derived for different layers of a sensor data
processing system to generate actions within the system's context.
This input data itself depends on a given sensor model to compute its
specific raw data. Amongst others, on the example of laser scanners
and camera systems, algorithms using modern graphical processing units
are outlined to generate the required raw data even for complex
situations.
To realize the aforementioned aspects, a development environment is
necessary consisting of tools for modeling and working with instances
of a domain specific language. Furthermore, a software framework is
required which provides easily usable and mature solutions for common
programming requirements like synchronization for concurrent threads
or communication in a high-level point of view. For relying on a
consistent and homogeneous software framework for implementing the
concepts, a highly portable and real-time-capable software framework
for distributed applications was realized which was written entirely
from scratch in strictly object-oriented C++. Moreover, this software
framework also integrates the formally modeled input data derived from
the specified requirements and the sensors' models to allow unattended
system simulations to support the acceptance tests for subsystems or
an entire system.
On the example of autonomous vehicles, the applicability of the
approach and the software framework is demonstrated by implementing a
vehicle navigation algorithm which uses a given digital map for
finding the best route to a desired destination from an arbitrarily
chosen starting point. This algorithm was developed considering the
test-first-principle and is continuously evaluated by unattended and
automatic software tests which are executed on a continuous
integration system. Its implementation as well as its evaluation make
use of the aforementioned concepts and algorithms. Therefore, the
vehicle's surroundings were formally modeled together with its
necessary sensors using the provided development tools and environment
for performing and evaluating unattended system runs before the
algorithm was put into operation on the real vehicle.