| Περίληψη |
Η συχνά τεράστια πολυπλοκότητα παράλληλων συστημάτων πραγματικού χρόνου κάνει πολύ δύσκολη τη σωστή σχεδίαση τους χωρίς κάποιας μορφής βοήθεια μέσω υπολογιστή. Σε αυτή την εργασία παρουσιάζουμε μια επέκταση του πολύ γνωστού μοντέλου επιλογής/απόφασης ( selection/resolution ή απλά ) AKS83a,AC85,GK80,Ku90,ABM86a η οποία συμπεριλαμβάνει χρονικούς περιορισμούς. Η επέκταση μας αποτελείται από μιά υλοποίηση ενός υπάρχοντος μοντέλου για χρονικές υποθέσεις και των αντίστοιχων αλγορίθμων Di89 μέσα στο μοντέλο. Περιγράφουμε τη χρήση και την υλοποίηση ενός νέου προγράμματος αυτόματης επαλήθευσης (verification) για συστήματα πραγματικού χρόνου με πεπερασμένες καταστάσεις το οποίο βασίζεται στο COSPAN, ένα πολύ γνωστό πρόγραμμα επαλήθευσης γιά παράλληλα συστηματα τα οποία είναι ανεξάρτητα από το χρόνο. Επεκτείνουμε το COSPAN προσθέτωντας μιά διεργασία ελεγκτή η οποία δημιουργείται αυτόματα και παρακολουθεί τους χρονικούς περιορισμούς, ώστε να αποκλείει συμπεριφορές του συστήματος που είναι χρονικά ασυνεπείς. Στην εργασία αρχικά παρουσιάζονται το μοντέλο και το COSPAN ως απαραίτητη υποδομή, το μοντέλο πραγματικού χρόνου, και η θεωρία και υλοποίηση των επεκτάσεων μας μέσω των οποίων χειριζόμαστε πληροφορία πραγματικού χρόνου. Στη συνέχεια συζητάμε τα αποτελέσματα της χρήσης του προγράμματος μας για τη λυση μερικών μη τετριμένων προβλημάτων. Το μοντέλο επιλογής/απόφασης είναι ένα μαθηματικό μοντέλο συγχρονισμού για συντρέχουσες διεργασίες, όπου ένα πολύπλοκο σύστημα μπορεί να περιγραφεί σαν ένα σύνολο από μηχανές πεπερασμένων καταστάσεων που συντονίζονται μεταξύ τους. Ενα χαρακτηριστικό, που κάνει το μοντέλο εξαιρετικά ελκυστικό, είναι ότι η σύζευξη των μηχανών περιγράφεται με κατηγορήματα (predicates) πάνω στα σήματα επικοινωνίας. Σε πολλές περιπτώσεις με αυτό τον τρόπο επιτυγχάνονται σύντομες, περιεκτικές και κατανοητές περιγραφές. Το μοντέλο είναι ένα μοντέλο διακριτού γραμμικού χρόνου. Ενας λογισμός ορίζεται πάνω σε διεργασίες οι οποίες συνθέτονται χρησιμοποιώντας τις πράξεις σύγχρονου ή ασύγχρονου γινομένου. Η επαλήθευση γίνεται προσθέτοντας συνθήκες αποδοχής στις διεργασίες εκφράζοντας έτσι επιθυμητές ιδιότητες του συστήματος, και/ή συνθήκες ζωτικότητας (liveness conditions). Το COSPAN HK89,KK86,HK90 είναι ένα εργαλείο λογισμικού για την περιγραφή και επαλήθευση συστημάτων που αποτελούνται από συντονιζόμενες συνιστώσες. Το COSPAN μπορεί να χρησιμοποιηθεί για την ανάπτυξη περιγραφών υψηλού επιπέδου, για την ανάλυση της λογικής και στοχαστικής συμπεριφοράς συστημάτων, και προαιρετικά για την παραγωγή πολύ αποδοτικών υλοποιήσεων σε κατευθείαν από την περιγραφή υψηλού επιπέδου. Το εργαλείο χρησιμοποιεί μια τυπική, ιεραρχική, αναλυτική μέθοδο ανάπτυξης. Η λογική ανάλυση στο COSPAN επιτυγχάνεται μέσω συμβολικού ελέγχου της περιγραφής του συστήματος ως προς την επιθυμητή συμπεριφορά που καθορίζει ο χρήστης. Το σύστημα δεν προσομοιώνεται ούτε υλοποιείται, αλλά κατασκευάζεται μια μαθηματική απόδειξη που επιβεβαιώνει (ή διαψεύδει) την ύπαρξη της υπό εξέταση συμπεριφοράς. Στους αλγόριθμους ανάλυσης του COSPAN χρησιμοποιούνται τυπικές τεχνικές αναγωγής που μπο να ανταπεξέλθουν στο συνήθως τεράστιο πλήθος καταστάσεων των συντονιζόμενων συστημάτων. Το μοντέλο επαυξάνεται ώστε να συμπεριληφθούν περιορισμοί πραγματικού χρόνου. Περιγράφουμε την έννοια των λογικών μετρητών χρόνου ( logical timers ) Di89 που είναι πλασματικές συνιστώσες και χρησιμοποιούνται για την παρακολούθηση των χρόνων κατά τους οποίους συμβαίνουν γεγονότα μέσα στο σύστημα. Με αυτό τον τρόπο είναι δυνατόν να αποκλειστούν υπολογιστικές ακολουθίες που παραβιάζουν τις χρονικές παραδοχές. Ετσι ένα σύστημα που μπορεί να παραβίαζε κάποιες προδιαγραφές συμπεριφοράς σε ένα μοντέλο που δεν λαμβάνει υπόψη τις σχετικές ταχύτητες των συνιστωσών, μπορεί να τις πληρεί κάτω από ορισμένες χρονικές παραδοχές. Στη συνέχεια παρέχουμε όλες λεπτομέρειες σχετικά με την υλοποίηση του μοντέλου διαδικασιών με χρόνο (timed processes) που κατασκευάζουμε χρησιμοποιώντας το COSPAN. Το νέο εργαλείο RTCOSPAN έχει υλοποιηθεί χωρίς τροποποιήσεις της εσωτερικής δομής του COSPAN ή της γραμματικής του δείχνοντας έτσι ότι επεκτάσεις καλά σχεδιασμένων εργαλείων επαλήθευσης είναι δυνατές. Το RTCOSPAN είναι συμβατό με το COSPAN. Παρουσιάζουμε το τμήμα της διασύνδεσης χρήστη-εργαλείου (user-interface) που εισάγει τα νέα χαρακτηριστικά του RTCOSPAN, τη φιλοσοφία σχεδίασης μέσω της οποίας το RTCOSPAN ανταπεξέρχεται το μεγάλο πλήθος καταστάσεων που απαιτούν οι μετρητές χρόνου, και δίνουμε αρκετές λεπτομέρειες των εσωτερικών δομών δεδομένων και αλγορίθμων του εργαλείου. Τέλος αναφέρουμε μερικά προβλήματα και περιορισμούς της τωρινής υλοποίησης μας. Η μέθοδος μας χρησιμοποιείται για την περιγραφή και επαλήθευση δύο συστημάτων. Το πρώτο μας παράδειγμα αποτελεί μιά επέκταση του γνωστού πρωτοκόλλου επικοινωνίας alternating--bit, η οποία περιέχει πληροφορία συνεχούς χρόνου. Το δεύτερο παράδειγμα χρησιμοποιεί δύο παράλληλα κανάλια επικοινωνίας με ακαθόριστη αλλά πεπερασμένη καθυστέρηση μετάδοσης. Για την ευκολία του αναγνώστη οι περιγραφές μας δίνονται με μορφή γράφων αντί για τη γλώσσα περιγραφής του RTCOSPAN, μια και η μετάφραση είναι απλή. Εχουμε δείξει ότι το COSPAN μπορεί να επεκταθεί ώστε να χειρίζεται περιορισμούς πεπερασμένων καθυστερήσεων με φυσικό τρόπο, και ότι το νέο σύστημα είναι σε θέση να επαληθεύσει ενδιαφέροντα παραδείγματα συστημάτων. Η βασική ιδέα του διαχωρισμού της περιγραφής σε τμήματα ανάλογα με την εξάρτηση από τον χρόνο, και η χρήση των περιοχών τιμών μετρητών για το κομμάτι που εξαρτάται από το χρόνο, μπορούν πιθανά να εφαρμοστούν και σε άλλες τεχνικές επαλήθευσης επίσης.
|
Επαλήθευση Συστήματος Πραγματικού Χρόνου - η Επέκταση του COSPAN σε Συνεχή Χρόνο
