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.
