- tr-announce - lists.rwth-aachen.de

2010-14: Lazy Abstraction for Size-Change Termination
by Carsten Fuhs 17 Aug '10

17 Aug '10

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.

1 0

2010-06: Computing maximum reachability probabilities in Markovian timed automata
by Carsten Fuhs 11 Aug '10

11 Aug '10

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.

1 0

2010-15: Termination Graphs for Java Bytecode
by Carsten Fuhs 31 Jul '10

31 Jul '10

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.

1 0

2010-05: Softwareunterstützung für adaptive eHome-Systeme
by Carsten Fuhs 26 Jul '10

26 Jul '10

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.

1 0

2010-13: Design Patterns for Safety-Critical Embedded Systems
by Carsten Fuhs 02 Jul '10

02 Jul '10

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.

1 0

2010-12: Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
by Carsten Fuhs 10 Jun '10

10 Jun '10

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.

1 0

2010-11: Parametric LTL Games
by Carsten Fuhs 01 Jun '10

01 Jun '10

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.

1 0

2010-09: The Structure of the Intersection of Tolerance and Cocomparability Graphs
by Carsten Fuhs 21 May '10

21 May '10

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}.

1 0

2010-10: Automated Termination Analysis for Logic Programs with Cut
by Carsten Fuhs 14 May '10

14 May '10

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.

1 0

2010-04: Management dynamischer Geschäftsprozesse auf Basis statischer Prozessmanagementsysteme
by Carsten Fuhs 26 Apr '10

26 Apr '10

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.

1 0