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.
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.
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%.
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.
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.
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.
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.
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).
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.
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.