δείτε την πρωτότυπη σελίδα τεκμηρίου στον ιστότοπο του αποθετηρίου του φορέα για περισσότερες πληροφορίες και για να δείτε όλα τα ψηφιακά αρχεία του τεκμηρίου*
SAT Solving as a Component for the F’ Flight Software Framework
Το λογισμικό έχει καθοριστικό ρόλο στη διασφάλιση της αποτελεσματικής λειτουργίας των αεροδιαστημικών συστημάτων. Καθώς τα συστήματα Λογισμικού Πτήσεων εξελίσσονται, η ικανότητα λήψης αποφάσεων σε πραγματικό χρόνο λαμβάνοντας παράλληλα υπόψη διάφορους περιορισμούς γίνεται όλο και πιο δύσκολη, ιδίως με πιο σύνθετα υποσυστήματα, όπως η ενσωμάτωση ρομποτικών συστημάτων. Οι SAT Solvers έχουν αναδειχθεί ως μια πρακτική εφαρμογή των τυπικών μεθόδων ανάλυσης, επιλύοντας σύνθετα προβλήματα που μπορούν να περιγραφούν με εξισώσεις Boolean. Η χρήση των SAT Solvers μπορεί να χρειαστεί να γίνει σε πραγματικό χρόνο, δηλαδή κατά τη διάρκεια λειτουργίας του Λογισμικού Πτήσης. Ωστόσο, η ενσωμάτωση των SAT Solver στις σύγχρονες αρχιτεκτονικές Λογισμικού Πτήσης μπορεί να αποτελέσει πρόκληση από την πλευρά της μηχανικής λογισμικού. Το F' (F prime) είναι ένα πρόσφατο πλαίσιο σε C++ από το Jet Propulsion Laboratory, για την ταχεία ανάπτυξη και ενσωμάτωση συστημάτων διαστημικών πτήσεων για αποστολές μικρής κλίμακας, όπως CubeSats ή όργανα. Σε αυτή τη μελέτη, παρουσιάζουμε την περίπτωση σχεδιασμού ενός SAT Solver Component βασισμένο στο F', από τις προδιαγραφές έως και την αρχιτεκτονική για την ενσωμάτωσή του. Ο προτεινόμενος σχεδιασμός προορίζεται να φιλοξενήσει διαφορετικούς SAT Solvers, είτε σε διαστημικά είτε σε επίγεια τμήματα.
(EL)
Software has a critical role in ensuring safe and efficient operation of aerospace systems. As flight software systems advance, the ability to make decisions at runtime while considering various constraints becomes increasingly challenging, especially with more complex subsystems such as robotics being integrated. SAT solving has emerged as a practical application of formal methods, solving complex problems that can be described as Boolean formulae. SAT evaluation may need to occur at runtime, when flight software is operating. However, integration of SAT solvers to contemporary flight software architectures can be challenging from a software engineering standpoint. F' (F Prime) is a recent C++ framework by the Jet Propulsion Laboratory for the rapid development and deployment of small-scale spaceflight systems such as CubeSats or instruments. In this thesis, we show case the design of a SAT Solver component over F', from requirements to its integration. Our proposed grey-box design is intended to accommodate different solvers, potentially either within space or ground segments.
(EN)
*Η εύρυθμη και αδιάλειπτη λειτουργία των διαδικτυακών διευθύνσεων των συλλογών (ψηφιακό αρχείο, καρτέλα τεκμηρίου στο αποθετήριο) είναι αποκλειστική ευθύνη των αντίστοιχων Φορέων περιεχομένου.
Βοηθείστε μας να κάνουμε καλύτερο το OpenArchives.gr.
Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών
