Εφαρμογή Τυπικών Μεθόδων Στις Κινητές Επικοινωνίες

Abstract

Η διπλωματική αυτή έχει κύριο σκοπό την προσπάθεια καταγραφής των εφαρμογών των τυπικών μεθόδων στην προδιαγραφή και την επαλήθευση ιδιοτήτων και χαρακτηριστικών των συστημάτων κινητών επικοινωνιών και συγκεκριμένα γίνεται μια προσπάθεια εφαρμογής πάνω στο πρωτόκολλο του Bluetooth.Αρχικά, στο πρώτο μέρος της διπλωματικής δίνουμε τις κύριες προδιαγραφές του Bluetooth και αναλύουμε εις βάθος κάποιες στοιβάδες του πρωτοκόλλου τις οποίες και θα μοντελοποιήσουμε με την βοήθεια των τυπικών μεθόδων. Στο δεύτερο μέρος γίνεται μια παρουσίαση των τυπικών μεθόδων και περιγράφεται ένα υποσύνολο τους, που αφορά τις αλγεβρικές γλώσσες προδιαγραφών και το μαθηματικό τους υπόβαθρο (μαθηματική λογική). Στην συνέχεια παρουσιάζεται η προτεινόμενη επέκταση της αλγεβρικής γλώσσας προδιαγραφών CafeOBJ, η MobileOBJ, που στόχο έχει την δυνατότητα περιγραφής συστημάτων κινητών επικοινωνιών. Βάσει της MobileOBJ μοντελοποιούμε το πρωτόκολλο των συστημάτων Bluetooth και συγκεκριμένα δυο βασικά πρωτόκολλα της στοίβας, το LMP(Link Management Protocol) και το LC(Link Controller).