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

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