Πρώιμη επικύρωση διαστημικού συστήματος με χρήση του εργαλείου Compass
Creators: name: Μάνδαρας, Εμμανουήλ Αθανασίου
Publisher: name: Aristotle University of Thessaloniki
Year: 2015
Subjects: Επικύρωση
Διαστημικό Σύστημα
Επαλήθευση
Validation
Space System
Compass

description: Σκοπός της εργασίας ήταν η επικύρωση του δορυφόρου GOES I-M της NASA, με τη χρήση του εργαλείου Compass, το οποίο απευθύνεται ειδικά στο σχεδιασμό και την ανάλυση διαστημικών συστημάτων, αλλά και η ανάδειξη της σημασίας και σκοπιμότητας εκτέλεσης των διαδικασιών μοντελοποίησης και επαλήθευσης κατά τα πρώιμα στάδια της ανάπτυξης του συστήματος. Αρχικά, αναπτύχθηκαν οι έννοιες της σχεδίασης ενός διαστημικού συστήματος, των προβλημάτων που ανακύπτουν αλλά και των εφαρμοσμένων διαδικασιών τυπικής επαλήθευσης. Στη συνέχεια, αναλύθηκε διεξοδικά η αποστολή και η αρχιτεκτονική του δορυφόρου GOES I-M, προς κατανόηση των εξαρτημάτων που διαθέτει αλλά και του διαχωρισμού του σε υποσυστήματα. Επίσης, παρουσιάστηκαν οι προδιαγραφές και απαιτήσεις που χαρακτηρίζουν την επιχειρησιακή φύση του συγκεκριμένου δορυφορικού συστήματος, μέσα από τις κρίσιμες λειτουργίες που εκτελεί στο διάστημα. Ακόμη, περιγράφηκε συνοπτικά το εργαλείο Compass και η γλώσσα slim, την οποία χρησιμοποιεί στη σχεδίαση του μοντέλου του συστήματος. Αναφέρθηκαν στοιχεία τόσο για τη σύνταξη των μοντέλων του εργαλείου όσο και για την εισαγωγή σφαλμάτων στις αναλύσεις και τις τεχνικές επαλήθευσης που εφαρμόζονται. Έπειτα, αποσαφηνίστηκε η δομή του μοντέλου που αναπτύχθηκε και, μάλιστα, παρουσιάστηκαν με λεπτομέρεια και επεξηγήσεις όλα τα σχεδιασμένα μοντέλα των υποσυστημάτων του δορυφόρου. Στο τέλος, αναλύθηκαν τα αποτελέσματα των εκτελεσθέντων επαληθεύσεων πάνω στις ιδιότητες που αφορούν συγκεκριμένες προδιαγραφές και λειτουργίες του συστήματος.
description: The aim of the thesis is the validation of GOES I-M, a satellite designed by NASA, using the Compass model checker, a toolset designated for space systems special design and analysis, and the emergence of the significance of modeling and verification execution during the early stages of a system’s development. At first, there was described the meaning of space system design, the problems emerging during that specific engineering, along with the formal verification techniques in use. Later, took place a complete description of the mission and architecture of the GOES I-M satellite, in order to get familiar with the typical components and the subsystems it consists of. Furthermore, there were presented the operational specifications and requirements of the satellite, in terms of crucial functions executed in space. Then, there was outlined the Compass toolset and the slim language, which is used in the modelling design of the system. All the features of the model syntax were mentioned, as well as the fault injections and the disposable analyses of the toolset for execution. Finally, the structure of the developed system model was clarified, and there were presented, in detail and along the appropriate explanations, all the satellite’s subsystem designed models. Finally, the results of all the verification analyses performed were mentioned, in terms of examining the designed properties concerning the satellite’s functions and specifications.