Formal techniques for realizability checking and synthesis of infinite-state reactive systems
Ανδρέας Κατής · 2025
Τα αντιδρώντα συστήματα είναι θεμελιώδη δομικά στοιχεία στην ανάπτυξη συστημάτων κρίσιμης ασφάλειας. Αποκαλούνται αντιδρώντα λόγω της αναγκαίας αλληλεπίδρασής τους με (ή εναντίον) ενός απρόβλεπτου και μη ελέγξιμου περιβάλλοντος, για ακαθόριστη χρονική διάρκεια. Συνεπώς, η επαλήθευση ενός κρίσιμου συστήματος εμπεριέχει την διαδικασία εκμαίευσης προδιαγραφών, δημιουργίας μοντέλων, υλοποίησης και δοκιμής αντιδρώντων υπο-συνιστωσών. Η έρευνα της τυπικής επαλήθευσης αντιδρώντων συστημάτων επιχειρεί να επιλύσει στοιχειώδη προβλήμα σε κάθε μια από αυτές τις διαδικασίες, με έμφαση στην δημιουργία μαθηματικών τεκμηρίων σχετικά με την ασφάλεια του συστήματος. Πιο σημαντικά, έχει αποδειχθεί πως η ύπαρξη τέτοιων τεκμηρίων μπορεί να οδηγήσει σε αξιόλογα επίπεδα εξοικονόμησης τόσο του χρόνου ανάπτυξης όσο και του κόστους παραγωγής συστημάτων. Η παρούσα διατριβή εξερευνεί το πρόβλημα της σύνθεσης αντιδρώντων συστημάτων όπου στόχος είναι η ανάπτυξη διαδικασιών απόφασης, ικανές για την απόδειξη (διάψευση) της πραγματοποιησιμότητας προδιαγραφών αντιδρώντων συστημάτων, καθώς και την παραγωγή στοιχείων που ουσιαστηκά αποτελούν αντιπροσωπευτικοί μάρτυρες της εκάστοτε απόφασης. Η σύνθεση αντιδρώντων συστημάτων είναι ένα πρόβλημα στενά συσχετιζόμενο με αυτό της τυπικής επαλήθευσης, αφού απαιτεί την ανάπτυξη σαφών, μαθηματικών τεκμηρίων πραγματοποιησιμότητας. Η συντρηπτική πλειοψηφία της διεξαγόμενης έρευνας σε αυτή την περιοχή έχει ως τώρα εστιάσει στην εφαρμογή της σε προδιαγραφές λογικής προτάσεων, όπου επιτρέπονται μόνο πράξεις στο πεδίο ορισμού της άλγεβρας Μπουλ. Στο πρώτο μέρος αυτής της διατριβής προτείνουμε καινοτόμους, αποδοτικούς αλγορίθμους σύνθεσης αντιδρώντων συστημάτων που επεκτείνουν την υποστήριξη σε προδιαγραφές λογικής προτάσεων έτσι ώστε να παράγουν υλοποιήσεις όταν οι προδιαγραφές εμπεριέχουν την χρήση πλουσιότερων θεωριών, όπως αριθμητικές πράξεις με ακέραιους και πραγματικούς αριθμούς. Συζητούμε τα πλεονεκτήματα και μειονεκτήματα κάθε αλγορίθμου συνοδεύοντας τις υλοποιήσεις τους με τυπική αποδείξεις της ορθότητάς τους. Στο δεύτερο μέρος της διατριβής εμβαθύνουμε σε ένα ανεξερεύνητο υποπρόβλημα της σύνθεσης αντιδρώντων συστημάτων, όπου παρουσιάζουμε την πρώτη προσπάθεια σύνθεσης συστημάτων για προβλήματα απείρων καταστάσεων στα οποία η υλοποίηση συμπεριφέρεται με αυθαίρετο και ποικιλόμορφο τρόπο. Παρότι τυπικά το αναμενόμενο προϊόν της σύνθεσης είναι ένας ντετερμινιστικός μάρτυρας, υποστηρίζουμε πως στην πράξη η τυχαιότητα στη συμπεριφορά μπορεί παραυτά να είναι πολύτιμη. Προς αυτόν τον σκοπό, αξιολογούμε την εφαρμογή υλοποίηση με αυθαίρετη συμπεριφορά σε προβλήματα συσχετιζόμενα με τη δοκιμή ασαφών δεδομένων (fuzz testing) και τον προγραμματισμό κινήσεως ρομπότ (robot motion planning), επιδεικνύοντας το πώς η σύνθεση αντιδρώντων συστημάτων μπορεί να χρησιμοποιηθεί με έναν πρωτότυπο τρόπο σε έννοιες μηχανικής λογισμικού που προηγουμένως δεν έχουν ληφθεί υπόψιν.