Αλγεβρική προδιαγραφή προτύπων

Abstract

Open standardization seems to be very popular among software developers as it simplifies the standard's adoption by the software engineering. Formal specification methods, while very promising, are being adopted very slowly as the industry seems to have little motivation to move into this territory. In this thesis, we will present the idea of applying formal specification techniques to (open) standards' specifications.We provide evidence for the advantages of the open standards formal specification over natural language documentations: Formal specifications are more concise, less ambiguous, more complete with respect to the original documentation and, when using certain kinds of specification languages, executable and reusable as they support module inheritance.The merging of formal specification methods and open standards allows i) a more concrete standard design; ii) an improved understanding of the environment under design; iii) an enforced certain level of precision into the specification, and also iv) provides software engineers with extended property checking/verification capabilities, especially if they opt to use any algebraic specification language.

Στη διδακτορική αυτή διατριβή θα εξετάσουμε την ιδέα της χρήσης Τυπικών Μεθόδων (και συγκεκριμένα Αλγεβρικών Προδιαγραφών) για τη δημιουργία τυπικών προδιαγραφών προτύπων για να συμπληρώσουν ή να αντικαταστήσουν τις προδιαγραφές που συνοδεύουν ένα πρότυπο και είναι γραμμένες σε κάποια φυσική γλώσσα, σε μια προσπάθεια να ελαχιστοποιηθούν τα λάθη κατανόησης τέτοιων κειμένων που οφείλονται κυρίως στην ασάφεια που εμπεριέχουν οι φυσικές γλώσσες. Οι προδιαγραφές αυτές μπορεί να είναι εκτελέσιμες, δίνοντάς μας έτσι τη δυνατότητα να περιγράψουμε και να επαληθεύσουμε την ισχύ κάποιων απαιτούμενων ιδιοτήτων του προτύπου.Οι Τυπικές Μέθοδοι είναι τεχνικές που χρησιμοποιούνται για την μοντελοποίηση (και επαλήθευση) περίπλοκων συστημάτων σε μορφή μαθηματικών οντοτήτων. Η κατασκευή ενός τέτοιου αυστηρού μαθηματικού μοντέλου επιτρέπει την επαλήθευση ιδιοτήτων του συστήματος με τρόπο πολύ πιο αναλυτικό και ενδελεχή από τον εμπειρικό έλεγχο. Τα πλεονεκτήματα της χρήσης Τυπικών Μεθόδων φαίνεται να αντισταθμίζονται κάπως από το υψηλό κόστος εφαρμογής τους, κάτι που κάνει τον ρυθμό αποδοχής τους από τη βιομηχανία πολύ αργό. Ισχυριζόμαστε πως η χρήση των τυπικών μεθόδων σε βιομηχανικά πρότυπα βοηθάει τόσο τη βιομηχανία, αφού κάνει τις προδιαγραφές των προτύπων πιο σαφείς και περιεκτικές, όσο και την κοινότητα των τυπικών Μεθόδων.