The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automated Termination Analysis of Java Bytecode by Term Rewriting
Carsten Otto, Marc Brockschmidt, Christian von Essen, Jürgen Giesl
AIB 2010-08
We present an automated approach to prove termination of Java
Bytecode (JBC) programs by automatically transforming them to
term rewrite systems (TRSs). In this way, the numerous
techniques and tools developed for TRS termination can now be
used for imperative object-oriented languages like Java, which
can be compiled into JBC.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
A New Intersection Model for Multitolerance Graphs, Hierarchy,
and Efficient Algorithms
George B. Mertzios
AIB 2010-07
Tolerance graphs model interval relations in such a way that
intervals can tolerate a certain degree of overlap without being in
conflict. This class of graphs has attracted many research efforts,
mainly due to its interesting structure and its numerous applications,
while a number of variations of this model has appeared. In particular,
one of the most natural generalizations of tolerance graphs, namely
\emph{multitolerance} graphs, has been introduced in 1998
\cite{Parra98}, where two tolerances are allowed for each interval.
These two tolerances - one from the left and one from the right side of
the interval - define an infinite number of the so called
\emph{tolerance-intervals}, which make the multitolerance model
inconvenient to cope with. The main subclass of multitolerance graphs,
namely bounded multitolerance graphs, coincide with the widely known
class of trapezoid graphs that has been extensively studied. In this
article we introduce the first non-trivial intersection model for
general multitolerance graphs, given by objects in the three-dimensional
space called \emph{trapezoepipeds}, which unifies in a simple and
intuitive way the trapezoid representation for bounded multitolerance
graphs and the recently introduced parallelepiped representation for
tolerance graphs \cite{MSZ-Model-SIDMA-09}. Apart from being important
on its own, this new intersection model proves to be a powerful tool for
designing efficient algorithms. Given a multitolerance graph with $n$
vertices and $m$ edges, we present three new algorithms that compute a
minimum coloring and a maximum clique in optimal $O(n\log n)$ time, and
a maximum weight independent set in $O(m + n\log n)$ time - this
algorithm also improves the best known running time of $O(n^{2})$ for
the same problem on tolerance graphs \cite{MSZ-Model-SIDMA-09}.
Moreover, we prove several structural results on the class of
multitolerance graphs, complementing thus the hierarchy of perfect
graphs given in \cite{GolTol04}. The resulting hierarchy of classes of
perfect graphs is \emph{complete}, i.e. all inclusions are strict.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
MontiCore: Agile Entwicklung von domänenspezifischen Sprachen
im Software-Engineering
Holger Krahn
AIB 2010-03
Domänenspezifische Sprachen (engl. domain specific language - DSL)
sind Sprachen der Informatik, mit denen kompakte Problemlösungen aus
eng umrissenen fachlichen oder technischen Anwendungsgebieten
formuliert werden können. Durch die Nutzung einer fachspezifischen
Notation gelingt die Integration von Experten einfacher als bei
einer herkömmlichen Softwareentwicklung, weil die Modelle von ihnen
besser verstanden werden.
Die automatische Erzeugung von Produktivcode aus domänenspezifischen
Modellen ist eine effektive Form der modellgetriebenen Entwicklung.
Die derzeitige DSL-Entwicklung erschwert aufgrund der fehlenden
zentralen Sprachreferenz, die die abstrakte und konkrete Syntax
umfasst, und der unzureichenden Modularisierung eine agile und
effiziente Vorgehensweise. Es mangelt an Methoden und
Referenzarchitekturen, um komplexe modellbasierte Werkzeuge
strukturiert entwerfen und in der Softwareentwicklung einsetzen zu
können.
In dieser Arbeit wird daher die DSL-Entwicklung mit dem
MontiCore-Framework beschrieben, das die modulare Entwicklung von
textuellen DSLs und darauf basierten Werkzeugen erlaubt.
Die wichtigsten wissenschaftlichen Beiträge lassen sich wie folgt
zusammenfassen:
* Die Definition von textuellen domänenspezifischen Sprachen wird
durch ein kompaktes grammatikbasiertes Format ermöglicht, das sowohl
die abstrakte als auch die konkrete Syntax einer Sprache definiert
und so als zentrale Dokumentation für die Entwickler und Nutzer einer
DSL fungiert. Die entstehende abstrakte Syntax entspricht etablierten
Metamodellierungs-Technologien und erweitert übliche
grammatikbasierte Ansätze.
* Die Wiederverwendung von Teilsprachen innerhalb der
modellgetriebenen Entwicklung wird durch zwei Modularitätsmechanismen
vereinfacht, da so existierende Artefakte auf eine strukturierte Art
und Weise in neuen Sprachdefinitionen eingesetzt werden können.
Grammatikvererbung erlaubt die Spezialisierung und Erweiterung von
Sprachen. Einbettung ermöglicht die flexible Kombination mehrerer
Sprachen, die sich auch in ihrer lexikalischen Struktur grundlegend
unterscheiden können.
* Das MontiCore-Grammatikformat ist modular erweiterbar, so dass
zusätzliche Informationen als so genannte Konzepte spezifiziert
werden können und darauf aufbauend weitere Infrastruktur aus der
Sprachdefinition generiert werden kann. Die Erweiterungsfähigkeit
wird durch Konzepte zur deklarativen Spezifikation von Links in der
abstrakten Syntax und durch ein Attributgrammatiksystem demonstriert.
* Die Entwicklung von Codegeneratoren und Analysewerkzeugen für DSLs
wird durch die Bereitstellung einer Referenzarchitektur entscheidend
vereinfacht, so dass bewährte Lösungen ohne zusätzlichen
Entwicklungsaufwand genutzt werden können. Die Qualität der
entstehenden Werkzeuge wird damit im Vergleich zu existierenden
Ansätzen gehoben.
* Es wird demonstriert, wie compilierbare Templates ein integriertes
Refactoring der Templates und einer Laufzeitumgebung ermöglichen.
Darauf aufbauend wird eine Methodik definiert, die aus exemplarischem
Quellcode schrittweise einen Generator entwickelt, dessen Datenmodell
automatisiert abgeleitet werden kann.
Die beschriebenen Sprachen und Methoden sind innerhalb des Frameworks
MontiCore implementiert. Ihre Anwendbarkeit wird durch die
Entwicklung des MontiCore-Frameworks im Bootstrapping-Verfahren und
durch zwei weitere Fallstudien demonstriert.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Learning Visibly One-Counter Automata in Polynomial Time
Daniel Neider, Christof Löding
AIB 2010-02
Visibly one-counter automata are a restricted kind of one-counter
automata:
The input symbols are typed such that the type determines the
instruction that is executed on the counter when the input symbol is
read. We present an Angluin-like algorithm for actively learning
visibly one-counter automata that runs in polynomial time in
characteristic parameters of the target language and in the size of
the information provided by the teacher.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies
Paul Hänsch, Michaela Slaats, Wolfgang Thomas
AIB 2009-18
Given a set $P$ of natural numbers, we consider infinite games where
the winning condition is a regular $\omega$-language parametrized by
$P$. In this context, an $\omega$-word, representing a play, has
letters consisting of three components: The first is a bit indicating
membership of the current position in $P$, and the other two
components are the letters contributed by the two players.
Extending recent work of Rabinovich we study here predicates $P$
where the structure $(\mathbb{N}, +1, P)$ belongs to the pushdown
hierarchy (or ``Caucal hierarchy''). For such a predicate $P$ where
$(\mathbb{N}, +1, P)$ occurs in the $k$-th level of the hierarchy,
we provide an effective determinacy result and show that winning
strategies can be implemented by deterministic level-$k$ pushdown
automata.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Vertex Splitting and the Recognition of Trapezoid Graphs
George B. Mertzios, Derek G. Corneil
AIB 2009-16
Trapezoid graphs are the intersection family of trapezoids where every
trapezoid has a pair of opposite sides lying on two parallel lines.
These graphs have received considerable attention and lie strictly
between permutation graphs (where the trapezoids are lines) and
cocomparability graphs (the complement has a transitive orientation).
The operation of ``vertex splitting'', introduced in~\cite{CC}, first
augments a given graph $G$ and then transforms the augmented graph by
replacing each of the original graph's vertices by a pair of new
vertices. This ``splitted graph'' is a permutation graph with special
properties if and only if $G$ is a trapezoid graph. Recently vertex
splitting has been used to show that the recognition problems for both
tolerance and bounded tolerance graphs is NP-complete~\cite{MSZ2}.
Unfortunately, the vertex splitting trapezoid graph recognition
algorithm presented in~\cite{CC} is not correct. In this paper, we
present a new way of augmenting the given graph and using vertex
splitting such that the resulting algorithm is simpler and faster than
the one reported in~\cite{CC}.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Learning Communicating and Nondeterministic Automata
Carsten Kern
AIB 2009-17
The results of this dissertation are two-fold. On the one hand,
inductive learning techniques are extended and two new inference
algorithms for inferring nondeterministic, and universal,
respectively, finite-state automata are presented. On the other hand,
certain learning techniques are employed and enhanced to
semi-automatically infer communicating automata (also called design
models in the software development cycle). For both topics,
theoretical results on the feasibility of the approaches, as well as
an implementation are presented which, in both cases, support our
theory.
Concerning the first objective to derive a so-called active online
learning algorithm for nondeterministic finite-state automata (NFA),
we present, in analogy to Angluin's famous learning algorithm L* for
deterministic finite-state automata (DFA), a version for inferring a
certain subclass of NFA. The automata from this class are called
residual finite-state automata (RFSA). It was shown by Denis et
al. that there is an exponential gap between the size of minimal DFA
and their corresponding minimal RFSA. Even if there are also cases
where the canonical (i.e., minimal) RFSA is exponentially larger than
a corresponding minimal NFA, we show that the new learning
algorithm---called NL*---is a great improvement compared to L* as the
inferred canonical RFSA has always at most the size of the
corresponding minimal DFA but is usually even considerably smaller and
more easy to learn. Unlike a learning procedure developed by Denis et
al.---called DeLeTe2---our algorithm is capable of deriving canonical
RFSA. Like L*, the new algorithm will be applicable in many fields
including pattern recognition, computational linguistics and biology,
speech recognition, and verification. From our point of view, NL*
might especially play a major role in the area of formal verification
where the size of the models that are processed is of enormous
importance and nondeterminism not regarded an unpleasant property.
The second objective of this thesis is to create a method for
inferring distributed design models (CFMs) from a given set of
requirements specified as scenarios (message sequence charts). The
main idea is to extend the L* algorithm to cope with valid and invalid
sets of system runs and, after some iterations, come up with an
intermediate design model (a DFA) which exhibits features that make it
distributable into communicating components (or processes) interacting
via FIFO channels. Theoretical results on which classes of CFMs are
learnable in which time-complexity bounds are presented. We also
developed a tool implementation called Smyle, realizing important
theoretical results evolving from this part of the thesis. Based on
this learning formalism we also derive a software-engineering
lifecycle model called the Smyle Modeling Approach in which we
embedded our learning approach.
Additionally, we launched a project for a new learning library called
libalf which includes most of the learning algorithms (and their
extensions) mentioned in this thesis. We hope that, due to its
continuously increasing functionality, libalf will find broad
acceptance among researchers, and that it will be the starting point
for an extensive project of different research groups which will
employ libalf, or augment the library with new algorithms.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Quantitative Model Checking of Continuous-Time Markov Chains
Against Timed Automata Specifications
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
AIB 2009-02
We study the following problem: given a continuous-time Markov
chain (CTMC) C, and a linear real-time property provided as a
deterministic timed automaton (DTA) A, what is the probability
of the set of paths of C that are accepted by A (C satisfies A)?
It is shown that this set of paths is measurable and computing
its probability can be reduced to computing the reachability
probability in a piecewise deterministic Markov process (PDP).
The reachability probability is characterized as the least
solution of a system of integral equations and is shown to be
approximated by solving a system of partial differential
equations. For the special case of single-clock DTA, the system
of integral equations can be transformed into a system of linear
equations where the coefficients are solutions of ordinary
differential equations.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Empirical Studies for the Application of Agile Methods
to Embedded Systems
Dirk Wilking
AIB 2008-19
Agile Methods are a collection of software engineering techniques with
specific differences to traditional software engineering processes.
The main differences consist of rapid, cycle based development phases
setting the focus of attention on feedback of the source code being
developed. The results taken from user feedback, software reviews, or
other forms of software evaluation are used as a basis for changes
which comprise for example corrections of the user interface or the
adaption of the software architecture. Based on single techniques
taken from Agile Methods, their application to embedded systems
software engineering is empirically evaluated in this thesis.
The experiments and studies which have been conducted comprise the
techniques of refactoring, short releases, and test driven
development. The results hint to inconclusive effects. For example it
could be shown that a constant effort for functional work is achieved
by using the short releases technique, but its impact on the resulting
software remains difficult to assess. For refactoring a reduced
consumption of memory was found, but this effect was created by an
overhead for applying the refactoring technique itself.
The effect of agile techniques appears to be inferior to individual
software development ability of participants in terms of factor
strength. Consequently, the second part of the thesis aims at creating
variables for the purpose of experiment control. Variables comprise
C language knowledge and viscosity measuring a participant's level of
reluctance to change a fragment of source code.
An additional experiment consists of the replication of the N-version
programming experiment by Knight and Leveson. The original experiment
of independence between two program failures has been extended by an
additional factor of hardware diversity. By using different hardware
platforms, it has been expected to create mutual independent failures
which is not approved by experimental observations.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Compositional Abstraction for Stochastic Systems
Joost-Pieter Katoen, Daniel Klink, Martin Neuhäußer
AIB 2009-15
We propose to exploit three-valued abstraction to stochastic systems in
a compositional way. This combines the strengths of an aggressive
state-based abstraction technique with compositional modeling. Applying
this principle to interactive Markov chains yields abstract models that
combine interval Markov chains and modal transition systems in a natural
and orthogonal way. We prove the correctness of our technique for
parallel and symmetric composition and show that it yields lower bounds
for minimal and upper bounds for maximal timed reachability probabilities.