guest ::
| 001 | 229446 | ||
| 005 | 20250613112301.0 | ||
| 024 | 7 | _ | |2 Laufende Nummer |a 32736 |
| 024 | 7 | _ | |2 ISSN |a 0935-3232 |
| 024 | 7 | _ | |2 URN |a urn:nbn:de:hbz:82-opus-47785 |
| 024 | 7 | _ | |2 HSB |a 999910322688 |
| 024 | 7 | _ | |2 OPUS |a 4778 |
| 037 | _ | _ | |a RWTH-CONV-144416 |
| 041 | _ | _ | |a English |
| 082 | _ | _ | |a 004 |
| 100 | 1 | _ | |0 P:(DE-82)017688 |a Nguyen, Viet Yen |b 0 |e Author |
| 245 | _ | _ | |a Trustworthy spacecraft design using formal methods |c Viet Yen Nguyen |h online, print |
| 246 | _ | 3 | |a Zuverlässiger Entwurf von Raumfahrtsystemen mittels formaler Methoden |y German |
| 260 | _ | _ | |a Aachen |b Dep. of Computer Science, RWTH Aachen |c 2013 |
| 300 | _ | _ | |a 187 S. : graph. Darst. |
| 336 | 7 | _ | |0 PUB:(DE-HGF)11 |2 PUB:(DE-HGF) |a Dissertation / PhD Thesis |b phd |m phd |
| 336 | 7 | _ | |0 2 |2 EndNote |a Thesis |
| 336 | 7 | _ | |2 DRIVER |a doctoralThesis |
| 336 | 7 | _ | |2 BibTeX |a PHDTHESIS |
| 336 | 7 | _ | |2 DataCite |a Output Types/Dissertation |
| 336 | 7 | _ | |2 ORCID |a DISSERTATION |
| 336 | 7 | _ | |0 PUB:(DE-HGF)3 |2 PUB:(DE-HGF) |a Book |m book |
| 490 | 0 | _ | |a Aachener Informatik-Berichte |v 2012,17 |
| 500 | _ | _ | |a Zsfassung in dt. und engl. Sprache |
| 502 | _ | _ | |a Zugl.: Aachen, Techn. Hochsch., Diss., 2012 |g Fak01 |o 2012-12-04 |
| 520 | 3 | _ | |a Modellbasiertes Co-Engineering von Systemsoftware stellt einen natürlichen Evolutionsschritt zur Erfüllung der hohen Anforderungen zukünftiger Weltraum- und Satellitenmissionen dar. Es bietet bessere Abstraktionsmöglichkeiten zum Umgang mit wachsender Komplexität von Raumfahrzeugen und ermöglicht den Einsatz einer breiten Auswahl an formalen Methoden, die sich durch ihre mathematische Stringenz und Genauigkeit auszeichnen. Die vorliegende Dissertation behandelt sowohl Grundlagen als auch Anwendungen: Wir demonstrieren und evaluieren den Einsatz modernster Modellierungs- und Analysetechniken basierend auf formalen Methoden für die Raumfahrt und entwickeln neue Theorien zum Umgang mit Problemen in einem industriellen Umfeld. Konkret wird eine in der Luft-, Raumfahrt- und Automobilindustrie verbreitete Modellierungssprache namens “Architecture Analysis and Design Language” (AADL) formalisiert. Wir stellen ihre Verwurzelung in den Theorien der diskreten, Echtzeit- und Hybridautomaten, verschiedenen Markov-Modellen, sowie temporaler und probabilistischer Logik vor. Diese Grundlagen ermöglichen uns die Entwicklung eines umfangreichen Analysewerkzeugs basierend auf Modelcheckern. Es bietet eine breite Auswahl an algorithmischen Analysen anstatt der aufwändigen manuellen Methoden, welche zurzeit in der Raumfahrtindustrie eingesetzt werden. Dazu unterstützt es die vollautomatische Generierung und Analyse von Systemsimulationen, Fehlerbäumen, “failure modes and effects”-Tabellen, Wahrscheinlichkeitskurven, Diagnoseartefakten und Korrektheitsberprüfungen. Die Methoden werden durch ausführliche Evaluierungen validiert. Bei der Europäischen Raumfahrtagentur (ESA) wurden unsere Techniken während der Entwicklung einer zukünftigen Satellitenmission angewendet, deren Ergebnisse in der vorliegenden Dissertation behandelt werden. Diese Fallstudie ist die größte, in der Literatur erwähnte Studie zum Einsatz formaler Methoden zur Modellierung und Analyse einer Satellitenarchitektur. Die schiere Größe und Komplexität dieser Fallstudie stellte uns vor einige Probleme theoretischer Natur. Hierzu entwickelten wir Theorien zur Schlussfolgerung, basierend auf Craig-Interpolationen, die kompositionelle Abstraktionen des Modells generieren. Diese unterstützen das Verständnis großer Systemmodelle. Des Weiteren untersuchen wir die Verwendung von Krylov-Methoden zur Verbesserung der numerischen Stabilität bei der Analyse einer spezieller, sogenannter “steifer” Markov-Ketten. Diese treten häufig in Raumfahrtsystemen auf, bei denen die Ausfallraten von Komponenten große Diskrepanzen aufweisen. Unsere Experimente zeigen, dass Krylov-Methoden in diesen Fällen überlegen sind. |l ger |
| 520 | _ | _ | |a 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. |l eng |
| 591 | _ | _ | |a Germany |
| 650 | _ | 7 | |2 SWD |a Weltraumforschung |
| 650 | _ | 7 | |2 SWD |a Raumfahrt |
| 650 | _ | 7 | |2 SWD |a Raumfahrzeug |
| 650 | _ | 7 | |2 SWD |a Satellit |
| 650 | _ | 7 | |2 SWD |a Formale Methode |
| 650 | _ | 7 | |2 SWD |a Verifikation |
| 650 | _ | 7 | |2 SWD |a Validierung |
| 650 | _ | 7 | |2 SWD |a Modellierung |
| 650 | _ | 7 | |2 SWD |a Krylov-Verfahren |
| 650 | _ | 7 | |2 SWD |a Markov-Modell |
| 653 | _ | 7 | |a Informatik |
| 653 | _ | 7 | |2 ger |a Raumfahrtsysteme |
| 653 | _ | 7 | |2 ger |a Entwurf von Raumfahrtsystemen |
| 653 | _ | 7 | |2 ger |a Craig-Interpolation |
| 653 | _ | 7 | |2 eng |a formal methods |
| 653 | _ | 7 | |2 eng |a spacecraft design |
| 653 | _ | 7 | |2 eng |a verification and validation |
| 653 | _ | 7 | |2 eng |a modeling |
| 653 | _ | 7 | |2 eng |a satellite |
| 653 | _ | 7 | |2 eng |a safety and dependability |
| 653 | _ | 7 | |2 eng |a FTA |
| 653 | _ | 7 | |2 eng |a FMEA |
| 653 | _ | 7 | |2 eng |a Markov system software engineering |
| 653 | _ | 7 | |2 eng |a Krylov subspace methods |
| 653 | _ | 7 | |2 eng |a Craig interpolation |
| 700 | 1 | _ | |0 P:(DE-82)IDM00048 |a Katoen, Joost-Pieter |b 1 |e Thesis advisor |
| 856 | 4 | _ | |u https://publications.rwth-aachen.de/record/229446/files/4778.pdf |
| 909 | C | O | |o oai:publications.rwth-aachen.de:229446 |p VDB |p driver |p urn |p open_access |p openaire |p dnbdelivery |
| 915 | _ | _ | |0 StatID:(DE-HGF)0510 |2 StatID |a OpenAccess |
| 920 | 1 | _ | |0 I:(DE-82)120000_20140620 |k 120000 |l Fachgruppe Informatik |x 0 |
| 920 | 1 | _ | |0 I:(DE-82)121310_20140620 |k 121310 |l Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) |x 1 |
| 970 | _ | _ | |a HT017892558 |
| 980 | 1 | _ | |a FullTexts |
| 980 | _ | _ | |a phd |
| 980 | _ | _ | |a I:(DE-82)120000_20140620 |
| 980 | _ | _ | |a I:(DE-82)121310_20140620 |
| 980 | _ | _ | |a VDB |
| 980 | _ | _ | |a UNRESTRICTED |
| 980 | _ | _ | |a ConvertedRecord |
| 980 | _ | _ | |a FullTexts |
| 980 | _ | _ | |a book |
| Library | Collection | CLSMajor | CLSMinor | Language | Author |
|---|