Formal techniques for realizability checking and synthesis of infinite-state reactive systems

Abstract

Reactive systems are fundamental building blocks in the development of critical safety systems. The are called reactive due to the necessity of them interacting with (or against) an unpredictable and uncontrollable environment, for an indefinite amount of time. As a consequence, the verification of a critical system more often than not involves the process of writing requirements, modeling, implementing and testing reactive subcomponents. Research in formal verification for reactive systems attempts to solve fundamental problems in each of these processes, with an emphasis given on the creation of mathematical proofs regarding the system's safety. More importantly, it has been shown that such proofs can lead to significant savings both in development time as well as overall production cost. This dissertation explores the problem of reactive synthesis, where the goal is the development of decision procedures that are able to (dis)prove the realizability of reactive system specifications, as well as produce artifacts that essentially serve as witnesses to the decision. Reactive synthesis is a problem closely related to formal verification, as it requires the development of precise, mathematical proofs of realizability. The overwhelming majority of research conducted in this area has so far been focused in its application to propositional specification, where only operations over the Boolean domain can be performed. For the first part of this thesis, we propose novel, efficient reactive synthesis algorithms that extend the support for propositional specification to also generate implementations when the requirements involve the use of richer theories, such as integer and real arithmetic. We discuss the advantages and disadvantages of each algorithm, and accompany their implementation with a formal proof of soundness. In the second part of this dissertation, we delve into an unexplored sub-problem in reactive synthesis, where we present the first attempt ever to synthesize witnesses for infinite-state problems in which the implementation behaves in a random, diverse manner. While the product of synthesis is typically expected to be a deterministic witness, we argue that randomness can still be valuable in practice. To that end, we evaluate the application of randomly-behaving solutions to problems related to fuzz testing and robot motion planning, demonstrating how reactive synthesis can be used in an innovative way in software engineering concepts that have not been considered before.

Τα αντιδρώντα συστήματα είναι θεμελιώδη δομικά στοιχεία στην ανάπτυξη συστημάτων κρίσιμης ασφάλειας. Αποκαλούνται αντιδρώντα λόγω της αναγκαίας αλληλεπίδρασής τους με (ή εναντίον) ενός απρόβλεπτου και μη ελέγξιμου περιβάλλοντος, για ακαθόριστη χρονική διάρκεια. Συνεπώς, η επαλήθευση ενός κρίσιμου συστήματος εμπεριέχει την διαδικασία εκμαίευσης προδιαγραφών, δημιουργίας μοντέλων, υλοποίησης και δοκιμής αντιδρώντων υπο-συνιστωσών. Η έρευνα της τυπικής επαλήθευσης αντιδρώντων συστημάτων επιχειρεί να επιλύσει στοιχειώδη προβλήμα σε κάθε μια από αυτές τις διαδικασίες, με έμφαση στην δημιουργία μαθηματικών τεκμηρίων σχετικά με την ασφάλεια του συστήματος. Πιο σημαντικά, έχει αποδειχθεί πως η ύπαρξη τέτοιων τεκμηρίων μπορεί να οδηγήσει σε αξιόλογα επίπεδα εξοικονόμησης τόσο του χρόνου ανάπτυξης όσο και του κόστους παραγωγής συστημάτων. Η παρούσα διατριβή εξερευνεί το πρόβλημα της σύνθεσης αντιδρώντων συστημάτων όπου στόχος είναι η ανάπτυξη διαδικασιών απόφασης, ικανές για την απόδειξη (διάψευση) της πραγματοποιησιμότητας προδιαγραφών αντιδρώντων συστημάτων, καθώς και την παραγωγή στοιχείων που ουσιαστηκά αποτελούν αντιπροσωπευτικοί μάρτυρες της εκάστοτε απόφασης. Η σύνθεση αντιδρώντων συστημάτων είναι ένα πρόβλημα στενά συσχετιζόμενο με αυτό της τυπικής επαλήθευσης, αφού απαιτεί την ανάπτυξη σαφών, μαθηματικών τεκμηρίων πραγματοποιησιμότητας. Η συντρηπτική πλειοψηφία της διεξαγόμενης έρευνας σε αυτή την περιοχή έχει ως τώρα εστιάσει στην εφαρμογή της σε προδιαγραφές λογικής προτάσεων, όπου επιτρέπονται μόνο πράξεις στο πεδίο ορισμού της άλγεβρας Μπουλ. Στο πρώτο μέρος αυτής της διατριβής προτείνουμε καινοτόμους, αποδοτικούς αλγορίθμους σύνθεσης αντιδρώντων συστημάτων που επεκτείνουν την υποστήριξη σε προδιαγραφές λογικής προτάσεων έτσι ώστε να παράγουν υλοποιήσεις όταν οι προδιαγραφές εμπεριέχουν την χρήση πλουσιότερων θεωριών, όπως αριθμητικές πράξεις με ακέραιους και πραγματικούς αριθμούς. Συζητούμε τα πλεονεκτήματα και μειονεκτήματα κάθε αλγορίθμου συνοδεύοντας τις υλοποιήσεις τους με τυπική αποδείξεις της ορθότητάς τους. Στο δεύτερο μέρος της διατριβής εμβαθύνουμε σε ένα ανεξερεύνητο υποπρόβλημα της σύνθεσης αντιδρώντων συστημάτων, όπου παρουσιάζουμε την πρώτη προσπάθεια σύνθεσης συστημάτων για προβλήματα απείρων καταστάσεων στα οποία η υλοποίηση συμπεριφέρεται με αυθαίρετο και ποικιλόμορφο τρόπο. Παρότι τυπικά το αναμενόμενο προϊόν της σύνθεσης είναι ένας ντετερμινιστικός μάρτυρας, υποστηρίζουμε πως στην πράξη η τυχαιότητα στη συμπεριφορά μπορεί παραυτά να είναι πολύτιμη. Προς αυτόν τον σκοπό, αξιολογούμε την εφαρμογή υλοποίηση με αυθαίρετη συμπεριφορά σε προβλήματα συσχετιζόμενα με τη δοκιμή ασαφών δεδομένων (fuzz testing) και τον προγραμματισμό κινήσεως ρομπότ (robot motion planning), επιδεικνύοντας το πώς η σύνθεση αντιδρώντων συστημάτων μπορεί να χρησιμοποιηθεί με έναν πρωτότυπο τρόπο σε έννοιες μηχανικής λογισμικού που προηγουμένως δεν έχουν ληφθεί υπόψιν.