Στις 4 Ιανουαρίου ανακοινώθηκε η απονομή του βραβείου Turing 2007 στον Ιωσήφ Σηφάκη, Έλληνα ερευνητή που ζει και εργάζεται στην Grenoble της Γαλλίας, και στους Αμερικανούς ερευνητές Edmund Clarke (Carnegie Mellon University, USA) και Allen Emerson (University of Texas, Austin, USA), για τις εργασίες τους πάνω στο Model Checking, τεχνολογία επαλήθευσης συστημάτων πληροφορικής.

Το βραβείο Turing φέρει το όνομα του ’γγλου μαθηματικού Alan Turing ο οποίος θεωρείται θεμελιωτής της πληροφορικής και απονέμεται κάθε χρόνο από την ACM (Association for Computing Machinery). Επιβραβεύει ερευνητές για την ύψιστη συμβολή των ερευνών τους στην πληροφορική. Είναι η ανώτατη διάκριση στην πληροφορική, με κύρος ισάξιο ενός βραβείου Nobel.

Το Model Checking είναι μια αλγοριθμική μέθοδος επαλήθευσης η οποία επιτρέπει να καθοριστεί αν ένα μοντέλο, μέρος ενός συστήματος υλικού ή ενός σύνθετου λογισμικού, πληρεί τις σωστές προδιαγραφές, εκφρασμένες υπό κάποια μορφή λογικών προτάσεων. Επιπλέον, αν το μοντέλο δεν επαληθευτεί, η μέθοδος παράγει αντιπαραδείγματα τα οποία βοηθούν στον εντοπισμό της πηγής του προβλήματος.

H ιστορία του Model Checking

Οι θεωρητικές βάσεις του Model Checking τέθηκαν το 1981, από τους Edmund Clarke και Allen Emerson οι οποίοι εργαζόταν στις ΗΠΑ και τον Ιωσήφ Σηφάκη ο οποίος εργαζόταν ανεξάρτητα στην Γαλλία. Για να μπορέσει το Model Checking να χρησιμοποιηθεί επιτυχώς στην επαλήθευση πολυσύνθετων συστημάτων, χρειάστηκε να αναπτυχθούν θεωρητικά αποτελέσματα, μέθοδοι και εργαλεία για να αντιμετωπιστεί η πολυπλοκότητα του προβλήματος της «έκρηξης καταστάσεων» (state explosion).

Για την επίλυση του προβλήματος αξιοσημείωτn πρόοδος επιτεύχθηκε τα τελευταία 27 χρόνια από μια μεγάλη διεθνή επιστημονική κοινότητα. Τα επιτεύγματα αυτά βρίσκουν πολλές βιομηχανικές εφαρμογές στην επαλήθευση συστημάτων όπως επεξεργαστές, πρωτόκολλα επικοινωνιών, κρίσιμα συστήματα αυτόματου ελέγχου και κρυπτογραφικών αλγορίθμων που χρησιμοποιούνται στα αεροπλάνα, την αυτοκινητοβιομηχανία, το διάστημα και τις τηλεπικοινωνίες.

Οι εργασίες των Clarke, Emerson και Σηφάκη εξακολουθούν να είναι καθοριστικές για την επιτυχία αυτού του τομέα της έρευνας. Οδήγησαν στην δημιουργία νέων λογικών για την έκφραση προδιαγραφών και νέων αλγορίθμων επαλήθευσης. Εργαλεία που στηρίζονται στο Model Checking ανεπτυγμένα τόσο από πανεπιστημιακές καθώς και από βιομηχανικές ομάδες, αποτελούν την κύρια τεχνολογία για την επαλήθευση και την πιστοποίηση σύνθετων συστημάτων. Παραδείγματος χάριν, η τεχνολογία αυτή επιτρέπει συχνά στους μηχανικούς των ενσωματωμένων κυκλωμάτων να αναπτύξουν πολύπλοκα συστήματα με αυξημένη αξιοπιστία ως προς τις αρχικές απαιτήσεις. Αναμένεται ότι η συμβολή του Model Checking στην βιομηχανία θα είναι ακόμα πιο σημαντική στο μέλλον.

Ο Ιωσήφ Σηφάκης είναι διευθυντής έρευνας στο CNRS και ιδρυτής του εργαστηρίου Verimag στην Grenoble (http://www-verimag.imag.fr/). Είναι γνωστός για τις πρωτοποριακές εργασίες του, τόσο σε πρακτικό όσο και σε θεωρητικό επίπεδο, στην μοντελοποίηση των συστημάτων και την επαλήθευση τους. Οι τρέχουσες ερευνητικές του δραστηριότητες αφορούν τα συστήματα πραγματικού χρόνου υψηλής πιστότητας με εφαρμογές στα αεροπλάνα, το διάστημα, τα αυτοκίνητα και τις τηλεπικοινωνίες.

Ο Ιωσήφ Σηφάκης είχε ενεργό δράση στην μεταφορά των αποτελεσμάτων της έρευνας στην βιομηχανία, κυρίως σε συνεργασία με εταιρείες όπως η Airbus, Schneider Electric, STMicroelectronics και France Telecom.

www.kathimerini.gr