Αρχική | Oργανωτική Επιτροπή | Πρόγραμμα | Live | Presskit | Πρόσβαση | Φωτογραφίες | en

<<


Τυπικές Μέθοδοι και Ελεύθερο λογισμικό

Οι τυπικές μέθοδοι (formal methods) είναι ένα είδος υπολογιστικών τεχνικών (γλωσσών) που βασίζονται στα μαθηματικά και τη λογική και έχουν σημαντικές εφαρμογές στις προδιαγραφές, την ανάπτυξη και την επαλήθευση συστημάτων λογισμικού. Πολλές από τις τυπικές μεθόδους έχουν αναπτυχθεί μέσα στο περιβάλλον της ακαδημαϊκής και ερευνητικής κοινότητας και διέπονται από τη φιλοσοφία του ελεύθερου λογισμικού / λογισμικού ανοικτού κώδικα. Ο κώδικας των μεταφραστών των τυπικών μεθόδων είναι συνήθως ανοικτός. Αυτό έχει σαν αποτέλεσμα οι τυπικές μέθοδοι να είναι ανοικτές σε ελέγχους και βελτιώσεις από τη διεθνή επιστημονική κοινότητα. Σχεδόν το σύνολο των τυπικών μεθόδων διατίθεται δωρεάν. Συνήθως κάθε τυπική μέθοδος συνδέεται και με συγκεκριμένη μαθηματική σημασιολογία που στηρίζεται στη λογική. Έτσι, μπορούν να υποστηρίξουν την διερεύνηση της ορθότητας και την επαλήθευση προγραμμάτων και συστημάτων. Οι τυπικές μέθοδοι είναι χρήσιμες στην κοινότητα του ελεύθερου – ανοικτού λογισμικού για δύο τουλάχιστον βασικούς λόγους:

1) Μπορούν να χρησιμοποιηθούν για την επαλήθευση και πιστοποίηση της ορθότητας του λογισμικού ειδικά όταν αυτο χρησιμοποιείται για εφαρμογές που αφορούν στην ασφάλεια συστημάτων και εφαρμογές με μεγάλη πολυπλοκότητα.

2) Μπορούν να δημιουργήσουν νέα πεδία εφαρμογών του ελεύθερου / ανοικτού λογισμικού που να αφορούν την επαλήθευση προγραμμάτων και εφαρμογών λογισμικού, και την αυτόματη απόδειξη.

Η παρουσίασή μας θα περιλαμβάνει μια γενική εισαγωγή στις τυπικές μεθόδους και τη συνοπτική παρουσίαση μιας χαρακτηριστικής τέτοιας μεθόδου της γλώσσας αλγεβρικών προδιαγραφών CafeOBJ. Η γλώσσα αυτή αποτελεί την πιο σύγχρονη εκδοχή της γλώσσας OBJ (που αναπτύχθηκε στα πανεπιστήμια UCLA, Stanford, Oxford, UCSD) και αναπτύσσεται στην Ιαπωνία (JAIST). Θα παρουσιαστούν επίσης μια σειρά από χαρακτηριστικές εφαρμογές αυτής της γλώσσας στην επαλήθευση πρωτοκόλλων επικοινωνιών και εφαρμογών λογισμικού όπως έχουν αναπτυχθεί στο ΕΜΠ (ΣΕΜΦΕ, ΣΗΜΜΗΥ).

Ομιλητές: Πέτρος Στεφανέας (ΣΕΜΦΕ ΕΜΠ), Ιάκωβος Ουρανός (ΥΠΠΑ), Σπύρος Κομνηνός, Κώστας Μπάρλας, Κατερίνα Ξύστρα, Νίκος Τριανταφύλλου (ΣΗΜΜΗΥ ΕΜΠ)

Follow Me! Follow Me! Follow Me! Follow Me!