Systems verification using barrier certificates
Creators: name: Μιχάλογλου, Αλκμήνη Χριστόφορου
Publisher: name: Aristotle University of Thessaloniki
Year: 2020
Subjects: Φραγματικά Πιστοποιητικά
Επαλήθευση Συστημάτων
Αμετάβλητη
Barrier Certificates
System Verification
Invariant

description: A Barrier Certificate (BC) is a type of inductive invariant that can separate a system’s state space between safe and unsafe regions. It is a type of safety verification of systems. In this thesis, we explored BCs based on numerical computation. The works we elaborate on are: the convex condition, the exponential relaxation of the convex condition and, lastly, the research of Dai et al.,who provided two main contributions. First, they presented a General Barrier Condition that allows more approaches on BCs, and second, a new type of “combined” BC that utilizes two functions instead of one to serve as the invariant. BC description and conditions involve the change of the invariant’s sign when it alters between the safe and unsafe regions. This means that the main challenge when trying to synthesize a BC is the very hard problem of nonnegativity. In all computational approaches, Sum of Squares (SOS) and Semi-definite Programming(SDP) were used in order to deal with nonnegativity, since SOS can guarantee good solutions for it under certain circumstances. Therefore, the basic foundation of both these optimization methods is presented, along with guidelines and sources for thetools we worked with : SOSTOOLS and SeDuMi. We also provide the iterative algorithm of Dai et al for synthesizing BCs with additional information on how to use the algorithm in order to build a SOS program and practically utilize it. Finally we provide a code example, build upon code provided to us by the researchers cited, which is enriched with the proper commentary and guidelines. We implemented an example in this code, which showcases one of the biggest threats of BCs: SDP numerical errors.
description: Σε αυτή τη διπλωματική μελετήσαμε μία τεχνική επαλήθευσης συστημάτων: τα Φραγματικά Πιστοποιητικά (ΦΠ). Τα ΦΠ είναι επαγωγικές αμετάβλητες, συγκεκριμένα μαθηματικές συναρτήσεις, που μπορούν να διαχωρίσουν σαφώς τον χώρο καταστάσεων του συστήματος ανάμεσα σε ασφαλείς και μη ασφαλείς περιοχές. Τα ΦΠ που παρουσιάζουμε μπορούν να υπολογιστούν με αριθμητικούς υπολογισμούς και μεθόδους. Παρουσιάζουμε αναλυτικά τρεις ερευνητικές προσεγγίσεις: την αρχική “συνθήκη κυρτότητας”, την “εκθετική συνθήκη” και την “Γενική Συνθήκη Φράγματος” των Dai et al. η οποία περιγράφει περισσότερα ΦΠ . Παρουσιάζονται και τα συνδυαστικά ΦΠ. Η βασική πρόκληση που αντιμετωπίζουμε είναι το πρόβλημα “nonnegativity”, το πολύ δύσκολο πρόβλημα διατήρησης προσήμου καθώς η αμετάβλητη μεταβαίνει από ασφαλείς σε μη-ασφαλείς περιοχές. Σε κάθε υπολογιστική προσέγγιση, αξιοποιούνται μέθοδοι Αθροίσματος Τετραγώνων και Ημι-ορισμένου Προγραμματισμού για να διαχειριστούν το πρόβλημα αυτό, μιας και μπορούν να εγγυηθούν καλές λύσεις του υπό ορισμένες συνθήκες. Παρουσιάζουμε τα σχετικά εργαλεία SOSTOOLS και SeDuMi αντίστοιχα. Παρέχουμε τον αλγόριθμο των Dai et al. για σύνθεση ΦΠ, συνοδευόμενο από αναλυτικές οδηγίες για την μετάφραση του σε πρόβλημα Αθροίσματος Τετραγώνων και την πρακτική του εφαρμογή. Τέλος προσφέρουμε ένα παράδειγμα βασισμένο σε προϋπάρχουσα εφαρμογή και κώδικα (με την στήριξη των ερευνητών που το πρωτοδημιούργησαν) στο οποίο εφαρμόζονται οι τεχνικές που παρουσιάσαμε και αναδυκνείεται η αδυναμία των λογισμικών λύσης ημι-ορισμένου προγραμματισμού, τα αριθμητικά λάθη.