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

2014-05: Automated Termination Analysis for Programs with Pointer Arithmetic
by Thomas Ströder 31 Jan '14

31 Jan '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: Automated Termination Analysis for Programs with Pointer Arithmetic Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, and Peter Schneider-Kamp AIB 2014-05 While automated verification of imperative programs was studied intensively, proving termination of programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that represents all possible runs of the program. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.

1 0

2014-04: Languages of Infinite Traces and Deterministic Asynchronous Automata
by Thomas Ströder 31 Jan '14

31 Jan '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: Languages of Infinite Traces and Deterministic Asynchronous Automata Namit Chaturvedi AIB 2014-04 In the theory of deterministic automata for languages of infinite words, a fundamental fact relates the family of infinitary limits of regular languages and the family of omega-languages recognized by deterministic Buechi automata. With the known definitions of asynchronous automata, this observation does not extend to the context of traces. A major difficulty is posed by processes that stall after finitely many transitions. We introduce the family of deterministic, synchronization-aware asynchronous automata which -- using as parameter the set of processes that stay live ad infinitum -- allows us to settle an open question, namely, whether there exists a deterministic Buechi automaton recognizing precisely the infinitary limit of a regular trace language. Also, the corresponding class of unparameterized Muller automata captures all omega-Regular trace languages.

1 0

2013-19: Support for error tolerance in the Real-Time Transport Protocol
by Thomas Ströder 07 Jan '14

07 Jan '14

The following technical report is available from http://aib.informatik.rwth-aachen.de: Support for error tolerance in the Real-Time Transport Protocol Florian Schmidt, David Orlea, and Klaus Wehrle AIB 2013-19 Streaming applications often tolerate bit errors in their received data well. This is contrasted by the enforcement of correctness of the packet headers and payload by network protocols. We investigate a solution for the Real-time Transport Protocol (RTP) that is tolerant to errors by accepting erroneous data. It passes potentially corrupted stream data payloads to the codecs. If errors occur in the header, our solution recovers from these by leveraging the known state and expected header values for each stream. The solution is fully receiver-based and incrementally deployable, and as such requires neither support from the sender nor changes to the RTP specification. Evaluations show that our header error recovery scheme can recover from almost all errors, with virtually no erroneous recoveries, up to bit error rates of about 10%.

1 0

2012-17: Trustworthy Spacecraft Design Using Formal Methods
by Thomas Ströder 28 Oct '13

28 Oct '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: Trustworthy Spacecraft Design Using Formal Methods Viet Yen Nguyen AIB 2012-17 Model-based system-software co-engineering is a natural evolution towards meeting the high demands of upcoming deep-space and satellite constellation missions. It advocates better abstractions to cope with the increasing spacecraft complexity, and opens the door for a wide range of formal methods, benefiting from the mathematical rigour and precision they bring. This dissertation provides for both: we applied and evaluated state of the art modelling and analysis techniques based on formal methods to spacecraft engineering, and we developed novel theory that tackle issues encountered in industrial practice. In particular, we formalised a modelling language by the aviation and automotive industry, namely the Architecture Analysis and Design Language (AADL). We show in this dissertation how we rooted it into the theories on discrete, real-timed and hybrid automata, various Markov models and temporal and probabilistic logics. This foundation enabled us to develop a comprehensive analysis toolset with model checkers being the cornerstone. It provides a wide range of analyses in an algorithmic fashion rather than the labour-intensive methods currently employed by the space industry. It can generate simulations, fault trees, failure modes and effects tables, performability curves, diagnosability artefacts and affirmations of correctness exhaustively. Our work has been subjected to extensive evaluation. At the European Space Agency, we applied it to a satellite design of one of the agency's ongoing missions. This dissertation reports on this case study. The case is currently the largest formal methods study of a satellite architecture reported in literature. The sheer size and complexity of the satellite case study indicated several theoretical problems. To this end, we developed a reasoning theory based on Craig interpolants, that generates compositional abstractions from the model. It helps to understand large models, like the satellite case, more effectively. We furthermore studied the use of Krylov methods for improving the numerical stability of analysing a notorious class of Markov chains, namely, stiff Markov chains. They occur naturally in space systems where failure rates have large disparities. Our controlled experiments show that Krylov methods are superior in such cases.

1 0

2013-13: SensorCloud: Towards the Interdisciplinary Development of a Trustworthy Platform for Globally Interconnected Sensors and Actuators
by Thomas Ströder 24 Oct '13

24 Oct '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: SensorCloud: Towards the Interdisciplinary Development of a Trustworthy Platform for Globally Interconnected Sensors and Actuators Michael Eggert, Roger Häußling, Martin Henze, Lars Hermerschmidt, René Hummen, Daniel Kerpen, Antonio Navarro Pérez, Bernhard Rumpe, Dirk Thißen, and Klaus Wehrle AIB 2013-13 Although Cloud Computing promises to lower IT costs and increase users' productivity in everyday life, the unattractive aspect of this new tech- nology is that the user no longer owns all the devices which process personal data. To lower scepticism, the project SensorCloud investigates techniques to understand and compensate these adoption barriers in a scenario consisting of cloud applications that utilize sensors and actu- ators placed in private places. This work provides an interdisciplinary overview of the social and technical core research challenges for the trustworthy integration of sensor and actuator devices with the Cloud Computing paradigm. Most importantly, these challenges include i) ease of development, ii) security and privacy, and iii) social dimensions of a cloud-based system which integrates into private life. When these challenges are tackled in the development of future cloud systems, the attractiveness of new use cases in a sensor-enabled world will consider- ably be increased for users who currently do not trust the Cloud.

1 0

2013-12: Alternating Runtime and Size Complexity Analysis of Integer Programs
by Thomas Ströder 11 Oct '13

11 Oct '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: Alternating Runtime and Size Complexity Analysis of Integer Programs Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl AIB 2013-12 We present a modular approach to automatic complexity analysis. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer size bounds on program variables, we can restrict each analysis step to a small part of the program while maintaining a high level of precision. Extensive experiments with the implementation of our method demonstrate its performance and power in comparison with other tools.

1 0

2013-07: Ein modellbasiertes Sicherheitskonzept für die extrakorporale Lungenunterstützung
by Thomas Ströder 02 Oct '13

02 Oct '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: Ein modellbasiertes Sicherheitskonzept für die extrakorporale Lungenunterstützung André Stollenwerk AIB 2013-07 Die extrakorporale Lungenunterstützung (ECLA) als intensivmedizinische Behandlung des akuten progressiven Lungenversagens (ARDS) wird heutzutage nur als Ultima-Ratio-Therapie eingesetzt. Dies ist nicht zuletzt der Komplexität der Anwendung und den mit ihr verbundenen Risiken geschuldet. Zur Überwindung dieses Missstandes wurde das Projekt SmartECLA initiiert. Ziel war es, die Anwendung der ECLA durch konstruktive Verbesserungen, aber auch die Etablierung eines Regelungs- und Sicherheitskonzeptes für ein breiteres Anwendungsfeld zu öffnen. Die vorliegende Arbeit stellt ein Sicherheitskonzept für eine patientenorientiert geregelte ECLA vor. Das eingesetzte System wurde durch eine Fehlermöglichkeits- und -Einflussanalyse (FMEA) sowie eine Fehlerbaumanalyse (FTA) untersucht. Davon ausgehend wurden Modelle entwickelt, die helfen Fehlerereignisse zu erkennen und den Systemzustand abzuschätzen. Die erarbeiteten Modelle überwachen kontinuierliche Prozesse, wie die Abnutzung des eingesetzten Oxygenators oder die Rezirkulation innerhalb der Vena cava des Patienten durch die extrakorporale Zirkulation, aber auch diskrete Ereignisse wie das Ansaugen der Entnahmegefäßwand an die Kanüle oder Abweichungen der eingesetzten Blutpumpe von der zu erwartenden Charakteristik. Dadurch können Fehlerfälle gezielt erkannt werden. Die erarbeiteten Modelle adressieren methodisch die zuvor identifizierten möglichen Fehlerquellen, um so eine Gefährdung des Patienten, ausgehend von einer Fehlfunktion der eingesetzten Komponenten, zu unterbinden. Das Sicherheitskonzept wird auf einem Netzwerk aus dezentralen Sicherheitsknoten mithilfe einer eigens entwickelten Softwarearchitektur implementiert. Die Architektur ermöglicht eine effiziente Abschätzung - somit auch Planung - der zur Verfügung stehenden Ressourcen. Ein im Systemkonzept verankertes Datenmanagement ermöglicht dabei ausgehend von einem statischen Datenhaltungsmodul die Planung. Ausgehend von den durch die eingebetteten Anwendungen deklarierten Bedürfnissen werden nur die notwendigen Datenstrukturen bzw. Algorithmen in Code abgebildet. Neue Modelle und Anwendungen können durch variable Entwicklungspfade unter Verwendung der für sie effizientesten Werkzeuge und Umgebungen erstellt werden. Der entwickelte Systemaufbau fußt auf einer modularen, aber elektrisch robusten Hardwareplattform, die bedarfsorientiert an den jeweiligen Einsatzpunkt angepasst werden kann. Auf diese Weise können Energieverbrauch, Kosten und Entwicklungsaufwand minimiert werden. Eine auf der entworfenen Hardwareplattform basierende Weiterentwicklung ist die geschaffene Konsole zur Steuerung der eingesetzten Diagonalblutpumpe mit integrierter Blutflussregelung. Die in dieser Arbeit vorgestellten Ergebnisse machen einen Teil der benötigten Innovationen aus, welche es ermöglichten, im Rahmen des Projektes SmartECLA einen Machbarkeitsnachweis für die sichere Durchführung einer automatisierten ECLA zu erbringen.

1 0

2013-10: Performance Analysis of Computing Servers using Stochastic Petri Nets and Markov Automata
by Thomas Ströder 09 Sep '13

09 Sep '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: Performance Analysis of Computing Servers using Stochastic Petri Nets and Markov Automata Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, and Hao Wu AIB 2013-10 Generalised Stochastic Petri Nets (GSPNs) are a widely used modeling formalism in the field of performance and dependability analysis. Their semantics and analysis is restricted to "well-defined", i.e., confusion-free, nets. Recently, a new GSPN semantics has been defined that covers confused nets and for confusion-free nets is equivalent to the existing GSPN semantics. The key is the usage of a non-deterministic extension of CTMCs. A simple GSPN semantics results, but the question remains what kind of quantitative properties can be obtained from such expressive models. To that end, this paper studies several performance aspects of a GSPN that models a server system providing computing services so as to host the applications of diverse customers ("infrastructure as a service"). Employing this model with different parameter settings, we perform various analyses using the MaMa tool chain that supports the new GSPN semantics. We analyse the sensitivity of the GSPN model w.r.t. its major parameters --processing failure and machine suspension probabilities-- by exploiting the native support of non-determinism. The case study shows that a wide range of performance metrics can still be obtained using the new semantics, albeit at the prize of requiring more resources (in particular, computation time).

1 0

2013-08: On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers
by Thomas Ströder 04 Jul '13

04 Jul '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers Sebastian Junges, Ulrich Loup, Florian Corzilius and Erika Ábrahám AIB 2013-08 We address satisfiability checking for the first-order theory of the real-closed field (RCF) using satisfiability-modulo-theories (SMT) solving. SMT solvers combine a SAT solver to resolve the Boolean structure of a given formula with theory solvers to verify the consistency of sets of theory constraints. In this paper, we report on an integration of Gröbner bases as a theory solver so that it conforms with the requirements for efficient SMT solving: (1) it allows the incremental adding and removing of polynomials from the input set and (2) it can compute an inconsistent subset of the input constraints if the Gröbner basis contains 1. We modify Buchberger's algorithm by implementing a new update operator to optimize the Gröbner basis and provide two methods to handle inequalities. Our implementation uses special data structures tuned to be efficient for huge sets of sparse polynomials. Besides solving, the resulting module can be used to simplify constraints before being passed to other RCF theory solvers based on, e.g., the cylindrical algebraic decomposition.

1 0

2013-02: Modellbasierte Entwicklung automobiler Steuerungssysteme in Klein- und mittelständischen Unternehmen
by Thomas Ströder 06 May '13

06 May '13

The following technical report is available from http://aib.informatik.rwth-aachen.de: Modellbasierte Entwicklung automobiler Steuerungssysteme in Klein- und mittelständischen Unternehmen Michael Reke AIB 2013-02 Kleine und mittelständische Unternehmen (KMU) sind die Innovationsträger der Industrie. Dies gilt insbesondere für eine an Technologie orientierte Branche wie die Automobilindustrie. Für eine stärkere Integration von KMU in die Softwareentwicklung von Großunternehmen müssen jedoch viele Hürden überwunden werden, die aufgrund der großen strukturellen und kulturellen Unterschiede bestehen. So ist die Arbeit in den großen Unternehmen geprägt von stark reglementierten Prozessen und oft langwierigen Entscheidungswegen, die aufgrund der auf viele Mitarbeiter verteilten Entwicklung notwendig sind. Im Gegensatz dazu steht die Flexibilität und vergleichsweise einfache Prozessorganisation bei KMU, die oftmals zu kreativen Lösungen, schnellen Entscheidungen und einer kundenorientierten Arbeitsweise führen. Der in dieser Arbeit vorgestellte Ansatz für einen Entwicklungsprozess basiert auf Schnittstellen und Methoden der Prozesse, die von Großunternehmen verwendet werden. Die Prozesse selbst werden jedoch für den Einsatz in KMU vereinfacht, kombiniert und anders gewichtet. Das Ziel ist es dabei auf die Elemente zu verzichten, die eingeführt wurden, um die massiv parallele Entwicklung vieler Ingenieure zu organisieren. Die Prozesselemente, die hingegen eingeführt wurden, um eine hohe Softwarequalität zu erreichen, werden beibehalten. Dabei wird vorgestellt, dass insbesondere die modellbasierte Entwicklung geeignet ist, dieses Ziel zu unterstützen. Dafür wird zusätzlich zu der Prozessbeschreibung ein Entwicklungswerkzeug vorgestellt, das eine modellbasierte Softwareentwicklung ermöglicht. Die in dieser Arbeit diskutierten Prozesse wurden in einem kleinen Unternehmen für Entwicklungsdienstleistungen eingeführt und evaluiert. Zusätzlich wird dargestellt, dass die Prozesse die Ziele und Arbeitpraktiken erfüllen, die von der Automotive SPICE Assessment Methode gefordert werden. Zusätzlich werden Anforderungen für das unterstützende Entwicklungswerkzeug definiert und dessen Softwarearchitektur wird präsentiert. Das zentrale Element ist dabei eine Abstraktionsschicht, die die Hardwarekonfiguration von der Modellierungsumgebung trennt und die für Simulation und Codegenerierung notwendigen Parameter integriert. Zur Evaluation werden unterschiedliche Fallstudien aus dem Bereich elektronischer Steuergeräte für Automobilanwendungen vorgestellt, anhand derer der Einsatz des Werkzeugs, die Entwicklungsmethoden und die Schnittstellen zu externer Softwarewerkzeugen diskutiert werden. Insgesamt stellt diese Arbeit einen Ansatz vor, wie kleine und mittelständische Unternehmen einen werthaltigen Beitrag in der Entwicklung automobiler Steuerungssysteme liefern, wenn die eingesetzten Prozesse und Werkzeuge die besonderen Vorteile dieser Unternehmen unterstützen.

1 0