Επιδιόρθωση συστημάτων μεταβάσεων μέσω αφαίρεσης

Abstract

Given a transition system M and a specification formula f, the problem of model checking is to determine if M satisfies f. An extended problem of model checking is that of model repair. In the case that M violates f, the problem of model repair is to obtain a new model M΄, such that M΄ satisfies f. Moreover, the changes made to M to derive M΄ should be minimum with respect to all such M΄. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or even large state spaces. This thesis examines the problem of model repair for (i) Kripke structures and Computation Tree Logic and, (ii) probabilistic systems and reachability temporal logic properties. For Kripke structures, this thesis presents a framework for model repair that uses abstraction refinement to tackle state space explosion. The proposed framework aims to repair Kripke Structure models based on a Kripke Modal Transition System abstraction and a 3-valued semantics for CTL. An abstract-model-repair algorithm is introduced for which soundness and semi-completeness are proven, and its complexity class is studied. Moreover, a prototype implementation is presented to illustrate the practical utility of abstract model repair on an Automatic Door Opener system model and a model of the Andrew File System 1 protocol. For probabilistic systems, this thesis presents a framework based on abstraction and re#nement, which reduces the state space of the probabilistic system to repair at the price of obtaining an approximate solution. A metric space is defined over the set of DTMCs, in order to measure the differences between the initial and the repaired models. For the repair, this thesis introduces an algorithm and discusses its important properties, such as soundness and complexity. As a proof of concept, experimental results are provided for probabilistic systems with diverse structures of state spaces, including thewell-known Craps game, the IPv4 Zeroconf protocol, a message authentication protocol and the gambler's ruin model.

Έστω ένα σύστημα μεταβάσεων Μ και μια ιδιότητα φ, το πρόβλημα του ελέγχου μοντέλου είναι να ελέγξουμε αν το μοντέλο Μ ικανοποιεί την ιδιότητα φ. Μια επέκταση του προβλήματος αυτού είναι το πρόβλημα της επιδιόρθωσης μοντέλου. Στην περίπτωση που η ιδιότητα φ δεν ικανοποιείται στο μοντέλο Μ, το πρόβλημα της επιδιόρθωσης μοντέλου είναι να βρούμε ένα άλλο μοντέλο Μ΄ το οποίο να ικανοποιεί την ιδιότητα φ. Επιπλέον, οι αλλαγές που θα γίνουν στο M για να προκύψει το Μ΄ θα πρέπει να είναι οι ελάχιστες σε σχέση με όλα τα αντίστοιχα Μ΄. Όπως και στον έλεγχο μοντέλου, η έκρηξη του χώρου των καταστάσεων καθιστά σχεδόν αδύνατη την εφαρμογή της επιδιόρθωσης μοντέλου σε μοντέλα με πολύ μεγάλο χώρο καταστάσεων. Στη διατριβή αυτή εξετάζουμε το πρόβλημα της επιδιόρθωσης μοντέλου για (1) τις δομές Κρίπκε και Λογική Υπολογιστικού Δέντρου (ΛΥΔ) και, (2) για πιθανοκρατικά συστήματα και ιδιότητες πρόσβασης χρονικής λογικής. Για τις δομές Κρίπκε, η διατριβή αυτή παρουσιάζει ένα πλαίσιο για την επιδιόρθωση μοντέλου που χρησιμοποιεί αφαίρεση και βελτίωση για να αντιμετωπίσει το πρόβλημα της έκρηξης του χώρου των καταστάσεων. Το προτεινόμενο πλαίσιο έχει ως σκοπό την επιδιόρθωση δομών Κρίπκε βασιζόμενο στην χρήση ως αφαιρετικών μοντέλων των Τροπικών Συστημάτων Μεταβάσεων Κριπκε (ΤΣΜΚ) και μιας σημασιολογίας τριών τιμών της ΛΥΔ. Εισάγεται ένας αφαιρετικός αλγόριθμος επιδιόρθωσης για τον οποίο αποδεικνύεται η ορθότητα του και η μερική πληρότητα του καθώς και μελετάται η πολυπλοκότητα του. Επιπλέον, η υλοποίηση ενός πρωτοτύπου χρησιμοποιείται για να παρουσιάσει την πρακτική εφαρμογή του πλαισίου σε ένα σύστημα αυτόματος ανοίγματος πόρτας και στο πρωτόκολλο συστήματος αρχείων Andrew 1. Για τα πιθανοκρατικά συστήματα, αυτή η διατριβή παρουσιάζει ένα πλαίσιο βασισμένο στην αφαίρεση και στην βελτίωση, το οποίο μειώνει το χώρο καταστάσεων του συστήματος που πρόκειται να επιδιορθωθεί με το κόστος της εύρεσης μιας προσεγγιστικής λύσης. Ένας μετρικός χώρος ορίζεται στο σύνολο των ΑΜΔΧ, με σκοπό να μετρηθούν οι διαφορές μεταξύ των αρχικών και των διορθωμένων μοντέλων. Για την επιδιόρθωση, αυτή η διατριβή εισάγει έναν αλγόριθμο και μελετά τις πιο σημαντικές ιδιότητες του όπως η ορθότητα, η πληρότητα και η πολυπλοκότητα. Η πρακτική χρησιμότητα του πλαισίου επιδεικνύεται με την επιδιόρθωση τεσσάρων διαφορετικών πιθανοκρατικών μοντέλων με ποικιλομορφία στη δομή του χώρου των καταστάσεων.