The following technical report is available from
http://aib.informatik.rwth-aachen.de:
A New Intersection Model and Improved Algorithms for Tolerance Graphs
George B. Mertzios, Ignasi Sau, Shmuel Zaks
AIB 2009-05
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, which generalizes in a natural way both interval and
permutation graphs, has attracted many research efforts since their
introduction in~\cite{GoMo82}, as it finds many important applications
in constraint-based temporal reasoning, resource allocation, and
scheduling problems, among others. In this article we propose the first
non-trivial intersection model for general tolerance graphs, given by
three-dimensional parallelepipeds, which extends the widely known
intersection model of parallelograms in the plane that characterizes the
class of bounded tolerance graphs. Apart from being important on its
own, this new representation also enables us to improve the time
complexity of three problems on tolerance graphs. Namely, we present
optimal $\mathcal{O}(n\log n)$ algorithms for computing a minimum
coloring and a maximum clique, and an $\mathcal{O}(n^{2})$ algorithm for
computing a maximum weight independent set in a tolerance graph with $n$
vertices, thus improving the best known running times
$\mathcal{O}(n^{2})$ and $\mathcal{O}(n^{3})$ for these problems,
respectively.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Model-Based Construction of Embedded & Real-Time
Software - A Methodology for Small Devices
Alexander Nyßen
AIB 2009-03
While model-based software engineering - due to its increased abstraction
and its advantages in terms of traceability and analyzability - seems to
be the adequate means to deal with the increased complexity of software
that one faces today, it does not seem to have penetrated all domains yet,
in particular not the one of small embedded & real-time systems. Seeing
this problem caused by the fact that current model-based approaches do not
pay sufficient attention to the rather special technical, organizational,
and economical constraints in the respective domain, this work presents
an approach that explicitly takes these constraints into account.
MeDUSA, a model-based software construction method for small embedded &
real-time systems, is a principal item of the presented solution. To
face the strong technical constraints it was especially designed as an
instance-driven method, not incorporating any object-oriented concepts,
but forcing a class-based design that can be seamlessly transferred
into a procedural implementation, which is still state-of-the-art in
the regarded domain. To guarantee such a seamless transition MeDUSA was
furthermore designed to be a software construction rather than a mere
design method, explicitly also addressing the implementation activities,
and especially the transition from detailed design into source code. Being
organized around the use case concept, the method excels at being very
systematic and - inter alia by facilitating a continuous real-time
analysis - also at being especially aware about the stringent real-
time constraints that have to be faced in the domain of embedded &
real-time systems.
ViPER, the supporting tool prototype, forms the second essential part of
the solution. It offers generic support for MeDUSA's modeling activities
by providing a graphical UML modeling environment, as well as special
support for the specification and simulation of narrative, textual use
case details. It furthermore demonstrates dedicated methodical support by
embedding a hypertext documentation of MeDUSA's definition, by providing
implementations of the MeDUSA UML profiles and model constraints,
and by offering dedicated wizards to support the execution of certain
MeDUSA tasks.
Together with their underlying languages, the Unified Modeling Language
as well as the ANSI-C programming language, MeDUSA and ViPER thus form
an integrated methodology, which is founded on shared concepts and
principles. Especially developed to address above quoted constraints,
the methodology is applicable to a domain, which has pretty much been
elided so far.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Static Termination Analysis for Prolog
using Term Rewriting and SAT Solving
Peter Schneider-Kamp
AIB 2008-17
The most fundamental decision problem in computer science is the halting
problem, i.e., given a description of a program and an input, decide
whether the program terminates after finitely many steps or runs
forever on that input. While Turing showed this problem to be
undecidable in eneral, developing static analysis techniques that can
automatically prove termination for many pairs of programs and inputs
is of great practical interest.
This is true in particular for logic programming, as the inherent lack
of direction in the computation virtually guarantees that any
non-trivial program terminates only for certain classes of inputs.
Thus, termination of logic programs is widely studied and significant
advances have been made during the last decades. Nowadays, there are
fully-automated tools that try to prove termination of a given logic
program w.r.t. a given class of inputs. Nevertheless, there still
remain many logic programs that cannot be handled by any current
termination technique for logic programs that is amenable to
automation.
Another area where termination has been studied even more intensively is
term rewriting. This basic computation principle underlies the
evaluation mechanism of many programming languages. Significant
advances towards powerful automatable termination techniques during the
last decade have yielded a plethora of powerful tools for proving
termination automatically.
In this thesis, we show that techniques developed for proving
termination of term rewriting can successfully be adapted and applied
to analyze logic programs. The new techniques developed significantly
extend the applicability and the power of automated termination
analysis for logic programs. The work presented here ranges from
adapting techniques to work directly on logic programs to
transformations from logic programs to a specialized version of term
rewriting. On the logic programming side we also present a new
pre-processing approach to handle logic programs with cuts. On the term
rewriting side we show how to search for certain popular classes of
well-founded orders on terms more efficiently by encoding the search
into satisfiability problems of propositional logic.
The contributions developed in this thesis are implemented in tools for
automated termination analysis -- mostly in our fully automated
termination prover AProVE. The significance of our results is
demonstrated by the fact that AProVE has reached the highest score both
for term rewriting and logic programming at the annual international
Termination Competitions in all years since 2004, where the leading
automated tools try to analyze termination of programs from different
areas of computer science.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Empirical Evaluations of Safety-Critical Embedded Systems
Falk Salewski
AIB 2008-18
Embedded systems based on different types of hardware platforms are
nowadays increasingly used in safety-critical applications. These
different hardware platforms lead to fundamental differences in design,
particularly regarding the corresponding software.
In this work, potential influences of hardware platforms on safety
properties were gathered and open issues were identified. The most
relevant of these open issues were evaluated for popular embedded
hardware platforms (microcontroller, CPLD/FPGA). In detail, the impacts
of hardware platform selection on software diversity, encapsulation,
reviewability, reusability and the development according to ISO26262
were chosen for investigation. Furthermore, the approach of software
diversity was compared with a fault removal approach. The evaluation was
realized in form of six experiments conducted for this work. During
these evaluations, the following similarities and differences were
observed for the considered hardware platforms. Despite the diversity
between the hardware platforms, failures observed in the software
versions, which were developed for these different platforms, contained
high numbers of dependent (coincident) failures. Although failure
dependency between two versions was reduced by the use of diverse
hardware platforms, this effect was low. Most dependent failures were
identified as implementation independent so that improvements of the
software diversity by hardware diversity were limited. Thus, a
comparison of software fault tolerance with a fault removal approach
based on tests and reviews was conducted. As a result, different types
of failures were mitigated by these alternative approaches. On the other
hand, differences between microcontrollers and FPGAs were observed.
First, certain advantages of FPGAs with respect to encapsulation and
reuse of real-time functions could be demonstrated. Moreover,
differences regarding the reviewability of software versions written for
FPGAs and microcontrollers were observed. Finally, the development
according to ISO26262 revealed only minor differences between the
investigated hardware platforms but between the different safety
concepts of device supervision and function supervision.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
The MeDUSA Reference Manual, Second Edition
Alexander Nyßen, Horst Lichter
AIB 2008-07
MeDUSA (Method for UML2-based Construction of Embedded & Real-Time
Software) is a model-based software construction method targeting the
domain of small embedded & real-time software. MeDUSA was developed by
the Research Group Software Construction of the RWTH Aachen University
in close cooperation with the German ABB Corporate Research Centre. It
incorporates various practical experiences gained during the industrial
development of embedded software in ABB Business Unit Instrumentation.
Being Use Case-driven, MeDUSA systematically covers the software
construction lifecycle phase from the early requirements up
to implementation. Models are successively developed and employed
throughout all activities. By enforcing a class-based rather than an
object-oriented design, a smooth transition of the resulting design
model towards an implementation in a procedural programming language is
facilitated. This is essential, as procedural programming languages as the
C language are still state-of-the-art in the domain of small embedded &
real-time software.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Comparing recent network simulators: A performance evaluation study
Hendrik vom Lehn, Elias Weingärtner and Klaus Wehrle
AIB 2008-16
Ranging from the development of new protocols to validating analytical
performance metrics, network simulation is the most prevalent methodology
in the field of computer network research. While the well known ns-2
toolkit has established itself as the quasi standard for network
simulation, the successors are on their way. In this paper, we first
survey recent contributions in the field of network simulation tools as
well as related aspects such as parallel network simulation. Moreover,
we present preliminary results which compare the resource demands for
ns-3, JiST, SimPy and OMNeT++ by implementing the identical simulation
scenario in all these simulation tools.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
A New Algorithm for Finding Trees with Many Leaves
Joachim Kneis, Alexander Langer, Peter Rossmanith
AIB 2008-15
We present an algorithm that finds trees with at least k leaves in
undirected and directed graphs. These problems are known as Maximum
Leaf Spanning Tree for undirected graphs, and, respectively, Directed
Maximum Leaf Out-Tree and Directed Maximum Leaf Spanning Out-Tree in
the case of directed graphs.
The run time of our algorithm is O(poly(|V|) + 4^k k^2) on undirected
graphs, and O(4^k |V| |E|) on directed graphs. Currently, the fastest
algorithms for these problems have run times of O(poly(n) + 6.75^k
poly(k)) and 2^{O(k log k)} poly(n), respectively.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Model Checking Software for Microcontrollers
Bastian Schlich
AIB 2008-14
Software of microcontrollers is getting more and more complex. It is
mandatory to extensively analyze their software as errors can lead to
severe failures or cause high costs. Model checking is a formal method
used to verify whether a system satisfies certain properties.
This thesis describes a new approach for model checking software for
microcontrollers. In this approach, assembly code is used for model
checking instead of an intermediate representation such as C code.
The development of [MC]SQUARE, which is a microcontroller assembly code
model checker implementing this approach, is detailed. [mc]square has
a modular architecture to cope with the hardware dependency of this
approach. The single steps of the model checking process are divided
into separate packages. The creation of the states is conducted by a
specific simulator, which is the only hardware-dependent package. Within
the simulator, the different microcontrollers are modeled accurately.
This work describes the modeling of the ATMEL ATmega16 microcontroller
and details implemented abstraction techniques, which are used to tackle
the state-explosion problem. These abstraction techniques include lazy
interrupt evaluation, lazy stack evaluation, delayed nondeterminism,
dead variable reduction, and path reduction. Delayed nondeterminism
introduces symbolic states, which represent a set of states, into
[MC]SQUARE while still explicit model checking techniques are used.
Thus, we successfully combined explicit and symbolic model checking
techniques.
A formal model of the simulator, which we developed to prove the
correctness of abstraction techniques, is described. In this work, the
formal model is used to show the correctness of delayed nondeterminism.
To show the applicability of the approach, two case studies are
described. In these case studies, we used programs of different sizes.
All these programs were created by students in lab courses, during
diploma theses, or in exercises without the intention to use them for
model checking.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Improving Context-Sensitive Dependency Pairs
Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl
Gutierrez, Salvador Lucas, Peter Schneider-Kamp, René Thiemann
AIB 2008-13
Context-sensitive dependency pairs (CS-DPs) are currently the most
powerful method for automated termination analysis of context- sensitive
rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer
from two main drawbacks: (a) CS-DPs can be collapsing. This complicates
the handling of CS-DPs and makes them less powerful in practice. (b)
There does not exist a "DP framework" for CS-DPs which would allow to
apply them in a flexible and modular way. This paper solves drawback
(a) by introducing a new definition of CS-DPs. With our definition,
CS-DPs are always non-collapsing and thus, they can be handled like
ordinary DPs. This allows us to solve drawback (b) as well, i.e., we
extend the existing DP framework for ordinary DPs to context- sensitive
rewriting. We implemented our results in the tool AProVE and successfully
evaluated them on a large collection of examples.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Abstraction for stochastic systems by Erlang's method of stages
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf
AIB 2008-12
This paper proposes a novel abstraction technique based on Erlang's
method of stages for continuous-time Markov chains (CTMCs). As abstract
models Erlang-k interval processes are proposed where state residence
times are governed by Poisson processes and transition probabilities
are specified by intervals. We provide a three-valued semantics of CSL
(Continuous Stochastic Logic) for Erlang-k interval processes, and show
that both affirmative and negative verification results are preserved
by our abstraction. The feasibility of our technique is demonstrated
by a quantitative analysis of an enzyme-catalyzed substrate conversion,
a well-known case study from biochemistry.