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.