The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Lazy Abstraction for Size-Change Termination
Michael Codish, Carsten Fuhs, Jürgen Giesl, Peter Schneider-Kamp
AIB 2010-14
Size-change termination is a widely used means of proving termination
where source programs are first abstracted to size-change graphs which
are then analyzed to determine if they satisfy the size-change
termination property. Here, the choice of the abstraction is crucial
to the success of the method, and it is an open problem how to choose
an abstraction such that no critical loss of precision occurs. This
paper shows how to couple the search for a suitable abstraction and
the test for size-change termination via an encoding to a single SAT
instance. In this way, the problem of choosing the right abstraction
is solved en passant by a SAT solver. We show that for the setting of
term rewriting, the integration of this approach into the dependency
pair framework works smoothly and gives rise to a new class of
size-change reduction pairs. We implemented size-change reduction
pairs in the termination prover AProVE and evaluated their usefulness
in extensive experiments.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Computing maximum reachability probabilities in Markovian timed automata
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
AIB 2010-06
We propose a novel stochastic extension of timed automata, i.e.
Markovian Timed Automata (MTA). We study the problem of
optimizing the reachability probabilities in this model. Two
variants are considered, namely, the time-bounded and
unbounded reachability. In each case, we propose Bellman
equations to characterize the probability. For the former, we
provide two approaches to solve the Bellman equations, namely, the
discretization and a reduction to Hamilton-Jacobi-Bellman
equations. For the latter, we show that in the single-clock case,
the problem can be reduced to solving a system of linear
equations, whose coefficients are the time-bounded reachability
probabilities in CTMDPs.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Termination Graphs for Java Bytecode
Marc Brockschmidt, Carsten Otto, Christian von Essen, Jürgen Giesl
AIB 2010-15
To prove termination of Java Bytecode (JBC) automatically, we
transform JBC to finite termination graphs which represent all
possible runs of the program. Afterwards, the graph can be translated
into "simple" formalisms like term rewriting and existing tools can be
used to prove termination of the resulting term rewrite system (TRS).
In this paper we show that termination graphs indeed capture the
semantics of JBC correctly. Hence, termination of the TRS resulting
from the termination graph implies termination of the original JBC
program.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Softwareunterstützung für adaptive eHome-Systeme
Daniel Retkowitz
AIB 2010-05
eHomes sind Umgebungen, die sich durch eine Vernetzung der vorhandenen
Geräte auszeichnen, und in denen komplexe geräteübergreifende
Funktionalitäten in Form von Diensten angeboten werden. Übergreifende
Funktionalitäten gehören im Automobil bereits heute zum Standard, in
Wohnumgebungen sind sie jedoch bislang nicht verbreitet. Aber auch hier
gibt es verschiedenste Anwendungsfelder für solche Funktionalitäten, z.B.
in den Bereichen Sicherheit, Komfort, Multimedia, Kommunikation oder auch
bei der medizinischen Überwachung und der Unterstützung von Senioren.
Daher werden eHomes in Zukunft an Bedeutung gewinnen.
Für die Entwicklung von eHomes müssen eine Reihe von Herausforderungen
überwunden werden. Ein wesentlicher Aspekt ist die Berücksichtigung von
Mobilität und Dynamik in eHomes, die sich sowohl auf die Bewohner als auch
auf die Geräteumgebung beziehen. Da in eHomes eine Vielzahl von Standards
Anwendung finden, muss außerdem der daraus resultierenden Heterogenität
Rechnung getragen werden, um die Interoperabilität der Dienste zu
gewährleisten. Damit eHomes kostengünstig realisiert werden können, muss
insbesondere eine geeignete Infrastruktur bereitgestellt werden, die die
Entwicklung von Diensten und die Interaktion mit dem eHome-System
vereinfacht. Sowohl für die Dienstentwicklung als auch für den Betrieb von
eHomes sind daher geeignete Softwarewerkzeuge erforderlich.
Bisher wurde am Lehrstuhl für Informatik 3 (Softwaretechnik) der RWTH
Aachen bereits ein Ansatz erarbeitet, der die Entwicklung von eHome-
Diensten durch den Einsatz wiederverwendbarer Standardkomponenten für die
Dienstimplementierung vereinfacht. Im sogenannten SCD-Prozess, der sich
aus den Phasen Spezifizierung, Konfigurierung und Deployment
zusammensetzt, werden die Benutzerwünsche erfasst, und es wird darauf
basierend eine eHome-spezifische Dienstkomposition erstellt und dann zur
Ausführung gebracht. Ein entsprechendes Werkzeug unterstützt diesen
Prozess.
Die vorliegende Arbeit erweitert die bisherigen Konzepte durch Mechanismen
zur dynamischen Adaption. Dabei wird der bisherige SCD-Prozess, der die
Installationsphase eines eHomes abdeckt, zu einem kontinuierlichen SCD-
Prozess erweitert, der eine Unterstützung im laufenden Betrieb des eHomes
ermöglicht.
Die strukturelle Adaption dient der dynamischen Anpassung der
Dienstkomposition. Änderungen, die sich aus Mobilität und Dynamik ergeben,
können so zur Laufzeit berücksichtigt werden. Damit dies soweit möglich
automatisch durchgeführt werden kann, werden Erweiterungen der
Dienstspezifikation eingeführt, die es dem Entwickler erlauben, das
spätere Bindungsverhalten sowie mögliche Einschränkungen der Bindungen
festzulegen. Durch die neu eingeführten Mechanismen kann die
Mehrfachentwicklung von Querschnittsfunktionalitäten zur personen- und
kontextbezogenen Konfigurierung vermieden werden, was den Aufwand der
Dienstentwicklung reduziert.
Die semantische Adaption ermöglicht die Überwindung syntaktischer
Inkompatibilitäten, die sich aus der Heterogenität in eHomes ergeben. Dazu
wird die Dienstspezifikation um eine semantische Beschreibung ergänzt, die
die syntaktischen Elemente der Dienstschnittstellen auf semantische
Konzepte einer domänenspezifischen Ontologie abbildet. Dies schafft die
Grundlage für eine Dienstkomposition auf Basis semantisch
übereinstimmender Funktionalitäten. Ein im Rahmen der vorliegenden Arbeit
entwickelter Mechanismus zur automatischen Adaptergenerierung ermöglicht
die praktische Umsetzung des Ansatzes.
Die Ergebnisse dieser Arbeit liefern einen wissenschaftlichen Beitrag in
verschiedenen Bereichen. Der verfolgte Ansatz ist spezifisch auf die
Anwendungsdomäne eHomes ausgerichtet. Darin unterscheidet er sich von
anderen Ansätzen, die sich häufig mit allgemeinen Fragen der dynamischen
Dienstkomposition befassen. So ist eine gezieltere Unterstützung der
Besonderheiten im eHome möglich, z.B. bei der personen- und
kontextbezogenen Konfigurierung. Der kontinuierliche SCD-Prozess wird auf
Basis eines globalen Graphmodells in einem modellgetriebenen
Entwicklungsprozess realisiert. Die graphbasierten Techniken ermöglichen
dabei den einfachen Zugriff auf alle relevanten Daten. Das Graphmodell
wird außerdem für die Werkzeugentwicklung genutzt. Ein weiterer wichtiger
Beitrag dieser Arbeit ist der Laufzeitmechanismus zur dynamischen
Adaptergenerierung auf Basis der semantischen Dienstbeschreibung. Dieser
zeigt, wie mittels struktureller Reflection in Java eine Adaption zwischen
syntaktisch inkompatiblen Schnittstellen erreicht werden kann. Weitere
Ergebnisse sind ein Ansatz zur Laufzeitüberwachung der
Dienstkommunikation, für dessen Realisierung auf die aspektorientierte
Programmierung zurückgegriffen wird, und die Entwicklung von Werkzeugen,
die sowohl die Dienstentwicklung als auch die Laufzeit des eHome-Systems
abdecken.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Design Patterns for Safety-Critical Embedded Systems
Ashraf Armoush
AIB 2010-13
Over the last few years, embedded systems have been increasingly used
in safety-critical applications where failure can have serious
consequences. The design of these systems is a complex process, which
is requiring the integration of common design methods both in hardware
and software to fulfill functional and non-functional requirements for
these safety-critical applications.
Design patterns, which give abstract solutions to commonly recurring
design problems, have been widely used in the software and hardware
domain. In this thesis, the concept of design patterns is adopted in
the design of safety-critical embedded system. A catalog of design
patterns was constructed to support the design of safety-critical
embedded systems. This catalog includes a set of hardware and software
design patterns which cover common design problems such as handling of
random and systematic faults, safety monitoring, and sequence
control. Furthermore, the catalog provides a decision support
component that supports the decision process of choosing a suitable
pattern for a particular problem based on the available resources and
the requirements of the applicable patterns.
As non-functional requirements are an important aspect in the design
of safety-critical embedded systems, this work focuses on the
integration of implications on non-functional properties in the
existing design pattern concept. A pattern representation is proposed
for safety-critical embedded application design methods by including
fields for the implications and side effects of the represented design
pattern on the non-functional requirements of the systems. The
considered requirements include safety, reliability, modifiability,
cost, and execution time.
Safety and reliability represent the main non-functional requirements
that should be provided in the design of safety-critical applications.
Thus, reliability and safety assessment methods are proposed to show
the relative safety and reliability improvement which can be achieved
when using the design patterns under consideration. Moreover, a Monte
Carlo based simulation method is used to illustrate the proposed
assessment method which allows comparing different design patterns
with respect to their impact on safety and reliability.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Dependency Triples for Improving Termination Analysis of
Logic Programs with Cut
Thomas Ströder, Peter Schneider-Kamp, Jürgen Giesl
AIB 2010-12
In very recent work, we introduced a non-termination preserving
transformation from logic programs with cut to definite logic
programs. While that approach allows us to prove termination of a
large class of logic programs with cut automatically, in several
cases the transformation results in a non-terminating definite logic
program. In this paper we extend the transformation such that logic
programs with cut are no longer transformed into definite logic
programs, but into dependency triple problems. By the implementation
of our new method and extensive experiments, we empirically evaluate
the practical benefit of our contributions.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Parametric LTL Games
Martin Zimmermann
AIB 2010-11
We consider graph games of infinite duration with winning conditions
in parameterized linear temporal logic, where the temporal operators
are equipped with variables for time bounds. In model checking such
specifications were introduced as PLTL by Alur et al. and (in a
different version called PROMPT-LTL) by Kupferman et al..
Our work lifts their results on model checking for PLTL and PROMPT-LTL
to the level of games: we present algorithms that determine whether a
player wins a game with respect to some, infinitely many, or all
variable valuations. All these algorithms run in doubly-exponential
time; so, adding bounded temporal operators does not increase the
complexity compared to solving plain LTL games. Furthermore, we show
how to determine optimal valuations that allow a player to win a
game.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
The Structure of the Intersection of Tolerance and
Cocomparability Graphs
George B. Mertzios, Shmuel Zaks
AIB 2010-09
Tolerance graphs have been extensively studied since their
introduction in 1982 \cite{GoMo82}, due to their interesting structure
and their numerous applications, as they generalize both interval and
permutation graphs in a natural way. It has been conjectured in 1984
that the intersection of tolerance and cocomparability graphs
coincides with bounded tolerance graphs \cite{GolumbicMonma84}. The
conjecture has been proved for complements of trees, and later
extended to complements of bipartite graphs, and these are the only
known results so far. Furthermore, it is known that the intersection
of tolerance and cocomparability graphs is contained in the class of
trapezoid graphs. In this article we almost prove the conjecture given
in \cite{GolumbicMonma84}. Namely, we prove that the conjecture is
true for every graph $G$, whose tolerance representation $R$ satisfies
a slight assumption. This assumption is satisfied by a wide variety of
graph classes; for example, our results immediately imply the above
mentioned correctness of the conjecture for complements of bipartite
graphs. In particular, our assumption still holds if $R$ has exactly
one unbounded vertex, or even if for every unbounded vertex $u$ in $R$
there is no other unbounded vertex $v$, such that the neighborhood of
$v$ is strictly included in the neighborhood of $u$. Our results are
based on the intersection model of parallelepipeds in the
3-dimensional space for tolerance graphs, which has been recently
introduced in \cite{MSZ-Model-SIDMA-09}. The present article
illustrates how this intersection model can be used to derive also
structural results, besides its usefulness in the design of efficient
algorithms \cite{MSZ-Model-SIDMA-09}. The proofs of our results rely
on the fact that $G$ has simultaneously such a representation, as well
as a trapezoid representation. The techniques presented in this
article are new, provide geometrical insight for the structure of the
graphs that are both tolerance and cocomparability, and it can be
expected that they are extendable to the most general case, answering
in the affirmative the conjecture of \cite{GolumbicMonma84}.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automated Termination Analysis for Logic Programs with Cut
Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder,
Alexander Serebrenik, René Thiemann
AIB 2010-10
Termination is an important and well-studied property for logic
programs. However, almost all approaches for automated termination
analysis focus on definite logic programs, whereas real-world
Prolog programs typically use the cut operator. We introduce a
novel pre-processing method which automatically transforms Prolog
programs into logic programs without cuts, where termination of
the cut-free program implies termination of the original program.
Hence after this pre-processing, any technique for proving
termination of definite logic programs can be applied. We
implemented this pre-processing in our termination prover AProVE
and evaluated it successfully with extensive experiments.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Management dynamischer Geschäftsprozesse auf Basis
statischer Prozessmanagementsysteme
René Wörzberger
AIB 2010-04
Prozessmanagementsysteme dienen der Unterstützung von
Geschäftsprozessen. Sie versorgen dabei Prozessbeteiligte, wie
beispielsweise Sachbearbeiter oder Prüfsysteme in einer Versicherung,
zur richtigen Zeit mit relevanten Daten.
Komplexe Geschäftsprozesse sind nicht vollständig vor ihrer
Durchführung planbar. Unvorhersehbare Ereignisse erfordern, dass von
der in einem Prozessmodell festgehaltenen Planung während der
Prozessdurchführung abgewichen wird. Diese Eigenschaft von Geschäfts-
und Entwicklungsprozessen wird als Dynamik bezeichnet.
Gängige Prozessmanagementsysteme unterstützen die Dynamik in
Geschäftsprozessen nur unzureichend. Sie setzen voraus, dass ein
Geschäftsprozess vorab vollständig modelliert wird und legen somit vor
der Durchführung mögliche Abläufe fest. Abweichungen vom Prozessmodell
sind in ihnen nicht vorgesehen. Folglich ergeben sich hochkomplexe,
schlecht wartbare Prozessmodelle, die jedoch dem Anspruch ebenfalls
nicht genügen, jeden sinnvollen Prozessablauf abzudecken. Ergibt sich
aus fachlichen Notwendigkeiten bei der Prozessdurchführung ein Ablauf,
den das jeweilige Prozessmodell nicht vorsieht, müssen die
Prozessbeteiligten den Prozess entkoppelt von Prozessmanagementsystem
weiterführen. Das Prozessmanagementsystem kann dann jedoch nicht mehr
zur Unterstützung des Prozesses beitragen.
In dieser Arbeit wird ein Prozessmanagementsystem beschrieben, das
auch dynamische Prozesse unterstützt. Dynamische Änderungen können von
Prozessbeteiligten über strukturelle Änderungen an Modellen bereits
laufender Prozesse durchgeführt werden.
Im Gegensatz zu verwandten Arbeiten wurde das Prozessmanagementsystem
nicht von Grund auf neuentwickelt. Stattdessen erweitert es das
kommerzielle System IBM WebSphere Process Server, das von der Generali
Deutschland Informatik Services GmbH eingesetzt wird -- dem
kooperierenden Industriepartner dieser Arbeit. Hierdurch kann die
vorhandene Funktionalität des Process Servers weiterverwendet werden
und muss nicht reimplementiert werden.
Es wurden folgende Ergebnisse im Einzelnen erzielt:
Die unvollständige Modellwelt des Process Servers wurde
vervollständigt:
Prozessdefinitionsmodelle in der Standardsprache WS-BPEL werden
ergänzt um speziellere Prozessinstanzmodelle, die zusätzliche
Informationen über den aktuellen Ausführungszustand eines konkreten
Prozesses und dessen bisherige Prozesshistorie beinhalten. Abstrakter
als Prozessdefinitionsmodelle sind so genannte Prozesswissensmodelle,
in denen grobe Festlegungen über Abläufe in Prozessen getroffen
werden. Dazu gehören Festlegungen bzgl. Reihenfolgen bestimmter
Aktivitäten, deren gegenseitiger Ausschluss sowie
Ausführungshäufigkeiten bestimmter Aktivitäten in bestimmten
Prozessen. Sowohl die Syntax als auch die Semantik dieser drei
Prozessmodellarten wurde formal mithilfe von Metamodellen
bzw. Graphersetzungssystemen, Transitionssystemen und temporalen
Logikformeln beschrieben. Ein modellgetrieben entwickelter
Prozessmodelleditor dient zur Darstellung und Editierung von Modellen
aller drei Arten.
Die Semantikdefinition der Prozessdefinitions- und -instanzmodelle ist
Ausgangspunkt für die Realisierung einer den WebSphere Process Server
erweiternden, so genannten Dynamik-Schicht. Diese simuliert dynamische
Änderungen, die direkt im Process Server nicht vorgenommen werden
können. Die Simulation ist opak für Prozessbeteiligte, die dynamische
Änderungen als strukturelle Änderungen in Prozessinstanzmodellen
innerhalb des Prozessmodelleditors erfahren.
Dynamische Änderungen unterliegen technischen und fachlichen
Rahmenbedingungen. Ein syntaxbasiertes und im Prozessmodelleditor
implementiertes Prüfwerkzeug stellt sicher, dass Modelländerungen und
insbesondere dynamische Änderungen an Prozessinstanzmodellen, diese
Rahmenbedingungen nicht verletzen. Im Vergleich zu verwandten
Arbeiten, die technische und fachliche Regeln getrennt behandeln,
wurde in dieser Arbeit ein einheitlicher Ansatz gewählt, der beide
Regelarten berücksichtigt und auf der Object Constraint Language (OCL)
basiert. Das heißt, dass alle Modellarten auf innere (technische)
Korrektheit geprüft werden können, aber auch Prozessinstanzmodelle auf
Komplianz zu expliziten, fachlichen Rahmenbedingungen überprüft werden
können, die in Prozesswissensmodellen festgehalten sind.
Prüfungen gegen in Prozesswissensmodellen explizit modelliertes
Prozesswissen wurden durch Prüfungen gegen implizites Prozesswissen
ergänzt. Unter implizitem Prozesswissen wird in diesem Zusammenhang
Wissen über Ausführungshäufigkeiten und -reihenfolgen von Aktivitäten
verstanden, das sich in Prozessdefinitions- und -instanzmodellen
indirekt wiederfindet. In unterschiedlichen Prozessinstanz-
und -definitionsmodellen inkonsistent modellierte Abläufe werden
durch ein weiteres Prüfwerkzeug aufgedeckt. Dieses Prüfwerkzeug
basiert auf einer Graphgrammatik, die zwei Prozessinstanzmodelle
-- soweit möglich -- simultan ausführt und dabei erreichbare
Ausführungszustände in einem Transitionssystem festhält. Dieses
Transitionssystem ist Ausgangspunkt für einen Modellvergleich, der
Prozessbeteiligten detaillierte Informationen über inkonsistente
Abläufe in unterschiedlichen Prozessinstanzmodellen liefert.