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

2011-08: A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog
by Carsten Fuhs 08 Jul '11

08 Jul '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog Thomas Ströder, Fabian Emmes, Peter Schneider-Kamp, Jürgen Giesl, Carsten Fuhs AIB 2011-08 We present a new operational semantics for Prolog which covers all constructs in the corresponding ISO standard (including "non-logical" concepts like cuts, meta-programming, "all solution" predicates, dynamic predicates, and exception handling). In contrast to the classical operational semantics for logic programming, our semantics is linear and not based on search trees. This has the advantage that it is particularly suitable for automated program analyses such as termination and complexity analysis. We prove that our new semantics is equivalent to the ISO Prolog semantics, i.e., it computes the same answer substitutions and the derivations in both semantics have essentially the same length.

1 0

2011-11: Hierarchical Counterexamples for Discrete-Time Markov Chains
by Carsten Fuhs 13 May '11

13 May '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Hierarchical Counterexamples for Discrete-Time Markov Chains Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker AIB 2011-11 In this paper we introduce a novel counterexample generation approach for discrete-time Markov chains (DTMCs) with two main advantages: (1) We generate *abstract* counterexamples, which can be refined in a *hierarchical* manner. (2) We aim at minimizing the number of states involved in the counterexamples, and compute a *critical subsystem* of the DTMC, whose paths form a counterexample. Experiments show that with our approach we can reduce the size of counterexamples and the number of computation steps by orders of magnitude.

1 0

2011-03: A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems
by Carsten Fuhs 23 Apr '11

23 Apr '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems Lars Noschinski, Fabian Emmes, Jürgen Giesl AIB 2011-03 We present a modular framework to analyze the innermost runtime complexity of term rewrite systems automatically. Our method is based on the dependency pair framework for termination analysis. In contrast to previous work, we developed a direct adaptation of successful termination techniques from the dependency pair framework in order to use them for complexity analysis. By extensive experimental results, we demonstrate the power of our method compared to existing techniques.

1 0

2011-02: Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
by Carsten Fuhs 07 Apr '11

07 Apr '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting Marc Brockschmidt, Carsten Otto, Jürgen Giesl AIB 2011-02 In earlier work we presented an approach to prove termination of non-recursive Java Bytecode (JBC) programs automatically. Here, JBC programs are first transformed to finite termination graphs which represent all possible runs of the program. Afterwards, the termination graphs are translated to term rewrite systems (TRSs) such that termination of the resulting TRSs implies termination of the original JBC programs. So in this way, existing techniques and tools from term rewriting can be used to prove termination of JBC automatically. In this paper, we improve this approach substantially in two ways: (1) We extend it in order to also analyze recursive JBC programs. To this end, one has to represent call stacks of arbitrary size. (2) To handle JBC programs with several methods, we modularize our approach in order to re-use termination graphs and TRSs for the separate methods and to prove termination of the resulting TRS in a modular way. We implemented our approach in the tool AProVE. Our experiments show that the new contributions increase the power of termination analysis for JBC significantly.

1 0

2011-04: A Local Greibach Normal Form for Hyperedge Replacement Grammars
by Carsten Fuhs 19 Jan '11

19 Jan '11

The following technical report is available from http://aib.informatik.rwth-aachen.de: A Local Greibach Normal Form for Hyperedge Replacement Grammars Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll AIB 2011-04 Heap-based data structures play an important role in modern programming concepts. However standard verification algorithms cannot cope with infinite state spaces as induced by these structures. A common approach to solve this problem is to apply abstraction techniques. Hyperedge replacement grammars provide a promising technique for heap abstraction as their production rules can be used to partially abstract and concretise heap structures. To support the required concretisations, we introduce a normal form for hyperedge replacement grammars as a generalisation of the Greibach Normal Form for string grammars and the adapted construction.

1 0

2010-20: Degrees of Lookahead in Context-free Infinite Games
by Carsten Fuhs 29 Dec '10

29 Dec '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: Degrees of Lookahead in Context-free Infinite Games Wladimir Fridman, Christof Löding, Martin Zimmermann AIB 2010-20 We continue the investigation of delay games, infinite games in which one player may postpone her moves for some time to obtain a lookahead on her opponents moves. We show that the problem of determining the winner of such a game is undecidable for context-free winning conditions. Furthermore, we show that the necessary lookahead to win a context-free delay game cannot be bounded by an elementary function.

1 0

2010-19: Experimental Evaluation of an Independent Set Algorithm
by Carsten Fuhs 23 Dec '10

23 Dec '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: Experimental Evaluation of an Independent Set Algorithm Felix Reidl AIB 2010-19 Following up the development of the currently fastest Independent Set algorithm (Kneis, Langer, Rossmanith, 2009) we present a practical evaluation, both on real-world data taken from common biological problems and on synthetic data. In order to get a clearer picture we measure different aspects of our implementation, especially the different polynomial-time reduction rules. The main purpose of this report is to show that algorithms with provable upper bounds can indeed be used to solve practical instances, though some care must be taken in the transfer of algorithm to code.

1 0

2010-18: Personalisierte eHomes: Mobilität , Privatsphäre und Sicherheit
by Carsten Fuhs 25 Aug '10

25 Aug '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: Personalisierte eHomes: Mobilität, Privatsphäre und Sicherheit Ibrahim Armaç AIB 2010-18 eHomes sind intelligente Umgebungen, die ihren Benutzern durch die Kopplung von Geräte- und Softwarefunktionalitäten einen Mehrwert in Form von integrierten Diensten bieten. Der Mehrwert besteht darin, dass den Benutzern neuartige Funktionalitäten angeboten werden, die sie durch die getrennte Verwendung der einzelnen Geräte nicht erlangen könnten. Es existiert eine breite Palette von Anwendungsfeldern für eHome-Dienste wie etwa in den Bereichen Komfort, Sicherheit, Multimedia, Verbrauchserfassung oder betreutes Wohnen. Es gibt eine Reihe von Herausforderungen, die für die Entwicklung und den Betrieb von eHomes überwunden werden müssen. Um die Interoperabilität der Dienste zu gewährleisten, muss zunächst die aus der Vielzahl von unterschiedlichen Geräten und Standards resultierende Heterogenität bewältigt werden. Außerdem muss die hochgradige Dynamik berücksichtigt werden, um zur Betriebszeit auf Änderungen eingehen zu können, die sich etwa aus der Mobilität von Geräten und Benutzern ergeben. Weiterhin sind geeignete Konzepte zur Personalisierung erforderlich, um Funktionalitäten auf die individuellen Bedürfnisse der Benutzer anzupassen. Darüber hinaus muss die wechselseitige Sicherheit von Benutzern und eHomes gewährleistet werden. Zur Bewältigung der Heterogenitätsherausforderung wurden im Rahmen eines Forschungsprojekts am Lehrstuhl für Software Engineering (i3) an der RWTH Aachen bereits Konzepte und Werkzeuge für die Konfigurierung und den Betrieb von eHomes entwickelt. Hierfür wurde eine komponentenbasierte Softwarearchitektur entworfen, auf deren Basis Dienste flexibel und unverändert in mehreren eHomes wiederverwendet werden können. Die Wiederverwendung wird dabei durch den sogenannten SCD-Prozess unterstützt, der sich aus den drei Phasen Spezifizierung, Konfigurierung und Deployment zusammensetzt. In diesem Prozess kann auf Basis der erfassten Kundenwünsche komfortabel eine eHome-spezifische Dienstkomposition erstellt und zur Ausführung gebracht werden. Aufgrund des kontinuierlichen Charakters des SCD-Prozesses kann die Dienstkomposition im laufenden Betrieb eines eHomes an Änderungen im Rahmen der erwähnten Dynamik angepasst werden. Die vorliegende Arbeit ist im Rahmen dieses Projekts entstanden und betrachtet zwei signifikante Aspekte von eHomes, die in den Vorgängerarbeiten nicht behandelt wurden. Die erste Fragestellung betrifft die Unterstützung der Personalisierung im Rahmen der Inter-eHome-Mobilität, einer speziellen Art der Dynamik. Hierunter wird der Sachverhalt verstanden, dass Benutzer häufig zwischen verschiedenen eHomes wechseln. Ziel ist es, ihre Präferenzen in allen eHomes ohne mehrfachen Konfigurierungsaufwand soweit wie möglich zu berücksichtigen. Die im Rahmen dieser Arbeit neu entwickelten Konzepte ermöglichen die Personalisierung von eHomes auf zwei Arten: Erstens wird ein mobiles Benutzermodell entwickelt, mit dessen Hilfe die Benutzer ihre persönlichen Daten eHome-übergreifend auf einem mobilen Gerät verwalten und den jeweiligen eHomes zur Verfügung stellen können. Zweitens wird ermöglicht, dass die Benutzer eigene Dienste mitnehmen und auf ihren mobilen Geräten ausführen. Dadurch können sie gewohnte Funktionalitäten auch dann nutzen, wenn das besuchte eHome die Funktionalitäten nicht direkt über einen eigenen Dienst anbietet, obwohl es über die dafür nötigen Geräte verfügt. Die zweite Fragestellung bezieht sich auf die Gewährleistung der wechselseitigen Sicherheit im Rahmen dieser Mobilität. Es werden sowohl die Schutzziele der Benutzer als auch die der eHomes erfüllt. Um die Privatsphäre der Benutzer zu schützen, werden Konzepte entwickelt, die die Einhaltung der Prinzipien Datensparsamkeit und Unverkettbarkeit persönlicher Daten ermöglichen. Für die Realisierung der Datensparsamkeit gegenüber eHomes wird ein aushandlungsbasiertes Identitätsmanagementsystem eingeführt. Mithilfe dieses Systems können mobile Benutzer sowohl die Menge der einem eHome preisgegebenen Daten minimieren als auch jedem eHome gegenüber mit einer anderen Identität entgegentreten. Zur Realisierung der Datensparsamkeit gegenüber Diensten wird eine selektive Zugriffskontrolle für die Daten umgesetzt, die einem eHome bereits offengelegt wurden. Dadurch wird die Menge der einem Dienst zur Verfügung gestellten Daten auf ein notwendiges Minimum reduziert. Um eine Verkettbarkeit unterschiedlicher Identitäten durch mehrere eHomes auszuschließen, wird ein Authentifizierungsmechanismus auf Basis anonymer Credentials entwickelt. Eine mögliche Verkettbarkeit der Daten durch mehrere Dienste in einem eHome hingegen wird durch den Einsatz von Pseudonymen verhindert. Im Hinblick auf den Schutz von eHome-Diensten vor unbefugten Zugriffen werden zwei Arten von Zugriffen betrachtet. Für den Schutz vor dem Zugriff unbefugter Benutzer werden alternative Zugriffskontrollmechanismen entwickelt, die grob in Credential- und rollenbasierte Mechanismen unterteilt werden können. Sie erfüllen das Ziel der Zurechenbarkeit, das die Zuordnung von Aktivitäten zu den Benutzern ermöglicht, wenn dies erforderlich ist. Für den Schutz vor unbefugten Zugriffen durch Dienste wird eine rollenbasierte Zugriffskontrolle eingesetzt. Die Generierung und die dynamische Anpassung der Zugriffsrechte an eine sich zur Laufzeit ändernde Dienstkomposition findet dabei vollständig automatisch statt. Die beschriebenen Konzepte werden in Form neuer Werkzeuge umgesetzt. Die Anwendbarkeit der Ergebnisse dieser Arbeit wird durch ihre Evaluierung anhand von Testszenarien gezeigt. Hierfür werden verschiedene Demonstratoren herangezogen, die im Rahmen dieser Arbeit entwickelt wurden. Durch die Ergebnisse dieser Arbeit werden die einander widerstrebenden Anforderungen Schutz der Privatsphäre und Personalisierung miteinander in Einklang gebracht. Der entwickelte Lösungsansatz bietet hierfür einen guten Kompromiss zwischen Anonymität und Zurechenbarkeit. Insgesamt leistet diese Arbeit einen Beitrag zur Akzeptanz von eHomes, da mobile Benutzer durch die entwickelten Konzepte von den Vorteilen personalisierbarer Dienste in unterschiedlichen eHomes profitieren können, während ihre Privatsphäre geschützt bleibt.

1 0

2010-17: Systemmodell-basierte Definition objektbasierter Modellierungssprachen mit semantischen Variationspunkten
by Carsten Fuhs 25 Aug '10

25 Aug '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: Systemmodell-basierte Definition objektbasierter Modellierungssprachen mit semantischen Variationspunkten Hans Grönniger AIB 2010-17 Eine Voraussetzung für den Erfolg einer modellbasierten Methode zur Softwareentwicklung ist eine variable und dennoch präzise Definition der verwendeten Modellierungssprachen. Hierzu gehört insbesondere auch die explizite Definition der Bedeutung der Sprachen -- ihrer Semantik. Formale Semantik leistet einen wichtigen Beitrag zur unmissverständlichen Kommunikation zwischen den Beteiligten und kann einen hohen Grad der Automatisierung über interoperable Werkzeuge ermöglichen. Diese Arbeit beschäftigt sich mit der vollständigen, formalen Definition objektbasierter Modellierungssprachen und legt den Fokus auf die flexible Definition problemadäquater Semantik. Zur Definition der Semantik objektbasierter Modellierungssprachen wird das Systemmodell als von allen Sprachen gemeinsam genutzte semantische Domäne definiert. Das Systemmodell charakterisiert abstrakt die Struktur, das Verhalten und die Interaktion von Objekten objektbasierter Systeme. Die prädikative semantische Abbildung von Elementen der Syntax einer Sprache in das Systemmodell definiert für ein Modell eine Menge von objektbasierten Systemen und erzeugt damit eine präzise Bedeutung auch für unvollständige bzw. unterspezifizierte Modelle. Die Semantik von Modellkomposition und -verfeinerung kann auf Basis des Systemmodells durch einfache mathematische Operationen erklärt werden. Gemäß einer allgemeinen Klassifikation der möglichen Variabilität einer Modellierungssprache können die verschiedenen Sprachbestandteile wie Syntax, semantische Domäne und semantische Abbildung mit Varianten ausgestattet werden. Dies ermöglicht die Anpassung einer Sprache zum Beispiel an einen projektspezifischen Kontext. Varianten und ihre Abhängigkeiten werden in Feature-Diagrammen dokumentiert. Eine Konfiguration, also die Auswahl von Sprachvarianten gemäß der Feature-Diagramme, legt dann die Menge der gültigen Definitionen fest. Die eingeführte Werkzeugunterstützung basiert auf MontiCore, einem Framework zur modularen Erstellung von textuellen Modellierungssprachen und dem Theorembeweiser Isabelle/HOL. Hierdurch wird eine flexible und gleichzeitig maschinenlesbare Syntax und Semantik gewonnen. Auch die Definition und Konfiguration von Semantikvarianten wird unterstützt. Die Definition der Semantik der UML-Teilmenge UML/P dient der Erprobung des werkzeugunterstützten Vorgehens. Betrachtet werden Klassendiagrammen, Objektdiagramme, Statecharts und Sequenzdiagramme. Zudem werden als Aktions- bzw. Constraint-Sprache vereinfachte Versionen von Java und OCL verwendet. Die angegebenen Semantikvarianten können direkt zur maschinenunterstützten Verifikation im Theorembeweiser verwendet werden, da sich zusätzlich auch konkrete Modelle automatisch in Isabelle übersetzen lassen. Die Verifikation wird an Beispielen unter Verwendung integrierter Semantiken verschiedener Modellierungssprachen der UML/P demonstriert. Dies zeigt die praktische Verwendbarkeit des Ansatzes.

1 0

2010-16: Automating Acceptance Tests for Sensor- and Actuator-based Systems on the Example of Autonomous Vehicles
by Carsten Fuhs 25 Aug '10

25 Aug '10

The following technical report is available from http://aib.informatik.rwth-aachen.de: Automating Acceptance Tests for Sensor- and Actuator-based Systems on the Example of Autonomous Vehicles Christian Berger AIB 2010-16 In projects dealing with autonomous vehicles which are driving in different contexts like highways, urban environments, and rough areas, managing the software's quality for the entire data processing chain of sensor- and actuator-based autonomous systems is increasingly complex. One main reason is the early dependency on all sensor's raw data to setup the data processing chain and to identify subsystems. These sensors' data might be extensive, especially if laser scanners or color camera systems are continuously producing a vast amount of raw data. Moreover, due to this dependency the sensors' setup including their respectively specified mounting positions and calibration information is also necessary to gather real input data from real surroundings' situations of the system. This is even more important before actually starting to integrate independently developed subsystems for carrying out tests for the entire data processing chain. To reduce this dependency and therefore to decouple tasks from the project's critical path, an approach is outlined in this thesis which was developed to support the software engineering for sensor- and actuator-based autonomous systems. This approach relies on customer's requirements and corresponding customer's acceptance criteria as well as the decoupling of the software engineering from the real hardware environment to allow appropriate system simulations. Based on the customer's requirements, formally specified scenarios using a domain specific language are derived which are used to provide surroundings and suitable situations for a sensor- and actuator-based autonomous system. From these formally specified surroundings, the required input data is derived for different layers of a sensor data processing system to generate actions within the system's context. This input data itself depends on a given sensor model to compute its specific raw data. Amongst others, on the example of laser scanners and camera systems, algorithms using modern graphical processing units are outlined to generate the required raw data even for complex situations. To realize the aforementioned aspects, a development environment is necessary consisting of tools for modeling and working with instances of a domain specific language. Furthermore, a software framework is required which provides easily usable and mature solutions for common programming requirements like synchronization for concurrent threads or communication in a high-level point of view. For relying on a consistent and homogeneous software framework for implementing the concepts, a highly portable and real-time-capable software framework for distributed applications was realized which was written entirely from scratch in strictly object-oriented C++. Moreover, this software framework also integrates the formally modeled input data derived from the specified requirements and the sensors' models to allow unattended system simulations to support the acceptance tests for subsystems or an entire system. On the example of autonomous vehicles, the applicability of the approach and the software framework is demonstrated by implementing a vehicle navigation algorithm which uses a given digital map for finding the best route to a desired destination from an arbitrarily chosen starting point. This algorithm was developed considering the test-first-principle and is continuously evaluated by unattended and automatic software tests which are executed on a continuous integration system. Its implementation as well as its evaluation make use of the aforementioned concepts and algorithms. Therefore, the vehicle's surroundings were formally modeled together with its necessary sensors using the provided development tools and environment for performing and evaluating unattended system runs before the algorithm was put into operation on the real vehicle.

1 0