Ο έλεγχος μοντέλων (Model Checking), δηλαδή η τεχνολογία επαλήθευσης συστημάτων πληροφορικής, αποτελεί μία από τις επιστήμες αιχμής, προς αυτή την κατεύθυνση, καθώς μέσα από αυτή προκύπτουν ολοένα και περισσότερα «έξυπνα συστήματα», τα οποία αποτελούν πλέον αναπόσπαστο κομμάτι της ζωής μας με στόχο τη βελτίωση της ποιότητάς της, την εξοικονόμηση ενέργειας και χρημάτων και τη βέλτιστη διαχείριση των πόρων.
Ένας από τους διεθνώς αναγνωρισμένους Έλληνες ερευνητές στην υπολογιστική επιστήμη και στον τομέα του Model Checking, ο Ηρακλειώτης ηλεκτρολόγος μηχανικός Ιωσήφ Σηφάκης, βραβεύτηκε χθες με το μετάλλιο «Leonardo da Vinci», στο πλαίσιο του 40ου ετήσιου συνεδρίου της Ευρωπαϊκής Εταιρείας για την Εκπαίδευση των Μηχανικών (SEFI), που πραγματοποιείται στη Θεσσαλονίκη. Το μετάλλιο αυτό απονέμεται για πρώτη φορά σε Έλληνα επιστήμονα, ενώ έχουν ήδη τιμηθεί με αυτό προσωπικότητες όπως οι Ζακ Ντελόρ, Σαντιάγκο Καλατράβα κ.ά.
Ο κ. Σηφάκης, κάτοχος ήδη από το 2007 του βραβείου A.M. Turing, του αποκαλούμενου νόμπελ πληροφορικής, πρόκειται να τιμηθεί για την ερευνητική προσφορά του στην καλύτερη λειτουργία των έξυπνων υπολογιστικών συστημάτων. Εργάζεται για το Εθνικό Κέντρο Επιστημονικών Ερευνών της Γαλλίας, είναι διευθυντής έρευνας στο CNRS και ιδρυτής του εργαστηρίου Verimag στη Γκρενόμπλ.
Όπως ο ίδιος εξηγεί, το να κάνει κανείς ασφαλέστερα και πιο έξυπνα τα ήδη έξυπνα συστήματα, είναι καίριας σημασίας, καθώς οι εφαρμογές τέτοιων συστημάτων μπορούν να επηρεάσουν ακόμη και την ανθρώπινη ζωή, όταν για παράδειγμα χρησιμοποιούνται στην ιατρική και στην φαρμακευτική. Οι μεγάλες καινοτομίες στις περιπτώσεις αυτές αναμένονται στο άμεσο μέλλον, τόσο στη δημιουργία εξυπνότερων φαρμάκων, που θα δρουν πιο στοχευμένα, όσο και στην τηλεπαρακολούθηση ασθενών από απόσταση, χωρίς να απαιτείται νοσηλεία. «Στην ιατρική δεν υπάρχει περιθώριο λάθους των υπολογιστικών συστημάτων που χρησιμοποιούνται, καθώς από αυτά μπορεί να εξαρτάται η ανθρώπινη ζωή» σχολιάζει ο καθηγητής.
Πρωτοποριακές εργασίες
Ο Ιωσήφ Σηφάκης γεννήθηκε στο Ηράκλειο της Κρήτης το 1946, σπούδασε ηλεκτρολόγος μηχανικός στο Εθνικό Μετσόβιο Πολυτεχνείο και πληροφορική στο Πανεπιστήμιο της Γκρενόμπλ με γαλλική υποτροφία. Είναι γνωστός για τις πρωτοποριακές εργασίες του στη μοντελοποίηση των συστημάτων και την επαλήθευσή τους. Οι τρέχουσες ερευνητικές του δραστηριότητες αφορούν τα συστήματα πραγματικού χρόνου υψηλής πιστότητας με εφαρμογές στα αεροπλάνα, το διάστημα, τα αυτοκίνητα και τις τηλεπικοινωνίες. Το Model Checking είναι μια αλγοριθμική μέθοδος επαλήθευσης, η οποία επιτρέπει να καθοριστεί αν ένα μοντέλο, μέρος ενός συστήματος υλικού ή ενός σύνθετου λογισμικού, πληροί τις σωστές προδιαγραφές, εκφρασμένες υπό κάποια μορφή λογικών προτάσεων. Επιπλέον, αν το μοντέλο δεν επαληθευτεί, η μέθοδος παράγει αντιπαραδείγματα, τα οποία βοηθούν στον εντοπισμό της πηγής του προβλήματος.
