Μοντελοποίηση Και Επαλήθευση Κινητών Συστημάτων Με Τεχνικές Αλγεβρικών Προδιαγραφών

Abstract

Αντικείμενο της διατριβής αποτελεί η μοντελοποίηση και η επαλήθευση κινητών συστημάτων με χρήση τεχνικών αλγεβρικών προδιαγραφών. Με τον όρο κινητά συστήματα αναφέρονται τα συστήματα υπολογισμού ή/και επικοινωνιών στα οποία η έννοια της θέσης των αντικειμένων αποτελεί κρίσιμο χαρακτηριστικό τους και η μεταβολή της επηρεάζει καθοριστικά τη συμπεριφορά τους. Λόγω της ιδιαιτερότητας των συστημάτων αυτών, και εξαιτίας τη ραγδαίας εξάπλωσης της χρήσης των κινητών δικτύων και υπηρεσιών, οι απαιτήσεις για αξιοπιστία, ασφάλεια και λειτουργικότητα έχουν οδηγήσει στην ανάπτυξη τυπικών μεθόδων προσανατολισμένων στα κινητά συστήματα. Οι τυπικές μέθοδοι, οι οποίες είναι τεχνικές, γλώσσες και εργαλεία με ισχυρό μαθηματικό υπόβαθρο, μας δίνουν τη δυνατότητα μιας αυστηρής, μαθηματικά ορισμένης, χωρίς ασάφειες, περιγραφής ή προδιαγραφής των συστημάτων, η οποία χρησιμοποιείται για το σχεδιασμό τους, την ανάλυση, και την επαλήθευση επιθυμητών ιδιοτήτων τους. Ένας πολύ σημαντικός κλάδος των τυπικών μεθόδων είναι οι αλγεβρικές γλώσσες προδιαγραφών, οι οποίες έχουν ως μαθηματικό υπόβαθρο τους μαθηματικά λογικά συστήματα ή συνδυασμούς τους. Μια τέτοια εκτελέσιμη αλγεβρική γλώσσα προδιαγραφών νέας γενιάς, απόγονος των γλωσσών OBJ, είναι η CafeOBJ. Το βασικότερο χαρακτηριστικό της γλώσσας αυτής που τη διακρίνει από αντίστοιχους φορμαλισμούς, είναι η άμεση υποστήριξη που παρέχει στη συμπεριφοριακή προδιαγραφή με την ενσωμάτωση στο συντακτικό της ειδικών τύπων και τελεστών. Η συμπεριφοριακή προδιαγραφή, η οποία έχει τις βάσεις της στην άλγεβρα με κρυμμένους τύπους, υποστηρίζει την αλγεβρική προδιαγραφή με αντικείμενα ή αφηρημένες μηχανές καταστάσεων, δίνοντας τη δυνατότητα περιγραφής κατανεμημένων, δυναμικών συστημάτων με ταυτόχρονες διεργασίες. Παράλληλα, με χρήση τεχνικών επαλήθευσης που βασίζονται σε αυτή, μας δίνει τη δυνατότητα απόδειξης ιδιοτήτων ασφαλείας των συστημάτων που έχουν προδιαγραφεί.Με βάση τα παραπάνω, προτείνεται το πλαίσιο προδιαγραφής και επαλήθευσης κινητών συστημάτων MobileOBJ. Η προδιαγραφή του κινητού συστήματος, πρωτοκόλλου ή διαδικασίας, αποτελείται από τη σύνθεση τεμαχίων προδιαγραφών (specification modules) τα οποία περιγράφουν είτε τους τύπους δεδομένων, είτε το σύστημα σαν ένα Κινητό Παρατηρήσιμο Σύστημα Μετάβασης, ένα είδος συμπεριφοριακού αντικειμένου. Στη συνέχεια με βάση αυτή την προδιαγραφή και κάνοντας χρήση τεχνικών απόδειξης θεωρήματος είναι δυνατή η επαλήθευση ιδιοτήτων της. Το ότι ο δυναμικός χαρακτήρας του συστήματος προδιαγράφεται με εξισώσεις, κάνει τη μέθοδο αυτή καλύτερα κατανοητή και ευκολότερη από αντίστοιχες μεθόδους που προαπαιτούν βαθύτερη γνώση των τεχνικών απόδειξης θεωρήματος. Στη συνέχεια, επεκτείνοντας την αρχική προσέγγιση, δίνεται η δυνατότητα προδιαγραφής και φυσικών, συνεχών - πέραν των διακριτών - χαρακτηριστικών των κινητών συστημάτων, όπως ο χρόνος και η απόσταση. Τα παραπάνω επιτυγχάνονται με την ενοποίηση των Κινητών Παρατηρήσιμων Συστημάτων Μετάβασης με τα Χρονικά και τα Υβριδικά Παρατηρήσιμα Συστήματα Μετάβασης. Η εφαρμογή της μεθόδου παρουσιάζεται μέσα από τη μελέτη μιας σειράς περιπτώσεων που αντιστοιχούν σε συστήματα και πρωτόκολλα. Τα ζητήματα ασφαλείας για ένα κινητό σύστημα είναι μεγάλης κρισιμότητας και γι' αυτό το λόγο δεν θα μπορούσαν να παραβλεφθούν. Στα πλαίσια αυτά έχουν προδιαγραφεί και επαληθευθεί πρωτόκολλα ασφαλείας για ασύρματα δίκτυα αισθητήρων και πολύ-εκπομπής. Στο τελευταίο κομμάτι της διατριβής προτείνεται μια άλγεβρα πρωτοκόλλων για την επαναχρησιμοποίηση και σύνθεση πολύπλοκων πρωτοκόλλων από στοιχειώδη με βάση τις τεχνικές ιεραρχικής σύνθεσης αντικειμένων με χρήση συμπεριφοριακών αλγεβρικών προδιαγραφών και της άλγεβρας τεμαχίου προδιαγραφής. Αποδεικνύεται η διατήρηση ιδιοτήτων των στοιχειωδών πρωτοκόλλων στα σύνθετα πρωτόκολλα για τελεστές της άλγεβρας, και παρουσιάζονται παραδείγματα εφαρμογών της.