Safety-Critical Software Engineer, Rust and Ada SPARK

Ο ρόλος

Το AeroBrain είναι το σύνολο τεχνολογιών τεχνητής νοημοσύνης υψηλής διασφάλισης της SkyDynamics για την αεροδιαστημική και την άμυνα. Τα μέρη του ανταλλάσσουν δεδομένα με πρωτόκολλα που πρέπει να συμπεριφέρονται με τον ίδιο τρόπο κάθε φορά: ανάμεσα στα επίπεδα του λογισμικού, ανάμεσα στους κόμβους της βάσης LLiDA, και ανάμεσα στο αεροσκάφος, τη συσκευή στο άκρο του δικτύου και το έδαφος.

Σχεδιάζετε αυτά τα πρωτόκολλα και γράφετε το λογισμικό που τα υλοποιεί, στις γλώσσες που επιλέχθηκαν για τη διασφάλιση: Rust, Ada SPARK και C++. Όπου μια ιδιότητα μπορεί να αποδειχθεί, την αποδεικνύετε. Όπου δεν μπορεί, τη δοκιμάζετε και κρατάτε τα τεκμήρια.

Τι θα κάνετε

• Προδιαγραφή πρωτοκόλλων επικοινωνίας και συγχρονισμού: μηνύματα, καταστάσεις, χρονισμός και συμπεριφορά σε αστοχία.
• Υλοποίησή τους σε Rust, Ada SPARK και C++, με ασφάλεια μνήμης και με φραγμένη χρήση χρόνου και μνήμης.
• Απόδειξη των ιδιοτήτων που μετρούν (απουσία σφαλμάτων χρόνου εκτέλεσης, αναλλοίωτες του πρωτοκόλλου) με αποδείξεις SPARK και άλλη στατική ανάλυση.
• Εργασία με κανόνες κώδικα για λογισμικό κρίσιμο για την ασφάλεια και σύμφωνα με τους στόχους του DO-178C: απαιτήσεις, σχεδιασμός, κώδικας και δοκιμές με ιχνηλασιμότητα μεταξύ τους.
• Ορισμός των διεπαφών ανάμεσα στις γλώσσες (Rust, Ada, C και C++), ώστε οι εγγυήσεις να μη χάνονται στο όριο.
• Ανάπτυξη των δοκιμών: μονάδας, ολοκλήρωσης, έγχυσης σφαλμάτων και δομικής κάλυψης.
• Έλεγχος κώδικα και σχεδίων, και τήρηση του αρχείου που θα ζητούσε μια αρχή πιστοποίησης.

Τι φέρνετε

• 8 ή περισσότερα έτη επαγγελματικής εμπειρίας σε λογισμικό για συστήματα κρίσιμα για την ασφάλεια ή την αποστολή.
• Πολύ καλή γνώση Rust, μαζί με unsafe κώδικα, no_std και ενσωματωμένους στόχους.
• Ada και SPARK: συμβόλαια, απόδειξη απουσίας σφαλμάτων χρόνου εκτέλεσης, και τα προφίλ Ravenscar ή Jorvik.
• Πολύ καλή γνώση σύγχρονης C++ σε περιορισμένο υποσύνολο, όπως MISRA C++ ή AUTOSAR C++14.
• Σχεδιασμός και υλοποίηση πρωτοκόλλων: μηχανές καταστάσεων, σειριοποίηση, χρονισμός και συμπεριφορά σε απώλεια και αναδιάταξη μηνυμάτων.
• Εξοικείωση με το DO-178C και τα συμπληρώματά του, και με το MISRA C.
• Εμπειρία στην αεροπορία, την άμυνα, το διάστημα, την αυτοκινητοβιομηχανία, τους σιδηροδρόμους ή τα ιατροτεχνολογικά προϊόντα.
• Μεταπτυχιακό δίπλωμα (Master) στην επιστήμη υπολογιστών, στην ηλεκτρολογία ή τη μηχανική υπολογιστών, στα μαθηματικά, στη φυσική ή σε συναφές πεδίο.
• Ελληνικά, άριστη γνώση (απαραίτητη).
• Αγγλικά, άριστη γνώση (απαραίτητη).

Πρόσθετα προσόντα

• Διδακτορικό στην τεχνολογία λογισμικού, στις τυπικές μεθόδους, στις γλώσσες προγραμματισμού ή σε συναφές πεδίο.
• Τυπική προδιαγραφή και model checking: TLA+, Event-B, Frama-C ή παρόμοια.
• DO-333 (τυπικές μέθοδοι) και DO-330 (πιστοποίηση εργαλείων).
• Λειτουργικά συστήματα πραγματικού χρόνου και διαμερισμός κατά ARINC 653.
• Δίαυλοι δεδομένων αεροηλεκτρονικών: ARINC 429, ARINC 664, MIL-STD-1553 ή CAN.
• Κρυπτογραφικά πρωτόκολλα και ασφαλής επικοινωνία σε υλικό με περιορισμένους πόρους.
• Πιστοποιημένοι μεταγλωττιστές και αλυσίδες εργαλείων για Rust ή Ada.

Προϋποθέσεις

• Δικαίωμα εργασίας στην Ευρωπαϊκή Ένωση.
• Εκπληρωμένες στρατιωτικές υποχρεώσεις ή νόμιμη απαλλαγή, όπου αυτές ισχύουν για εσάς.