στον Γιάννη ΔΙΟΝΑΤΟ
O Edmund M. Clarke ξεκίνησε ως μαθηματικός. Τον κέρδισε όμως η Πληροφορική. Εργάστηκε ως ερευνητής με τεράστια συνεισφορά στο πολύ δύσκολο πρόβλημα της επαλήθευσης της ορθότητας προγραμμάτων που εκτελούν ζωτικές λειτουργίες όπως ο έλεγχος ενός αεροπλάνου ή ενός διαστημόπλοιου εν πτήσει.
Για την συνεισφορά του αυτή ο Ed Clarke τιμήθηκε το 2007 με το βραβείο Turing, που θεωρείται “το βραβείο Nobel της Πληροφορικής”, αλλά και με πλήθος άλλων βραβείων. Οι μέθοδοι και τα προγράμματα που ανέπτυξε για την γρήγορη και αποτελεσματική επαλήθευση της ορθότητας προγραμμάτων χρησιμοποιούνται ευρύτατα στη βιομηχανία και στην έρευνα σήμερα και έχουν συντελέσει στην ανίχνευση πλήθους “σκοτεινών” (δύσκολο δηλαδή να βρεθούν) λαθών, αποτρέποντας έτσι καταστροφές ή ακόμη και ανθρώπινες τραγωδίες.
Είναι καθηγητής στο φημισμένο Πανεπιστήμιο Carnegie Mellon των ΗΠA και βρίσκεται από εχθές, Δευτέρα, 13 Οκτωβρίου, στη Κρήτη, όπου θα αναγορευτεί επίτιμος διδάκτορας του Πανεπιστημίου Κρήτης. O Ed Clarke έχει ιδιαίτερες σχέσεις με αυτό το Πανεπιστήμιο, που ούτως ή άλλως είναι το κατ’ εξοχή ερευνητικό πανεπιστήμιο στην Ελλάδα: ένας από τους παλιούς του φοιτητές, ο Χρήστος Νικολάου, είναι καθηγητής εκεί, πρώην πρύτανης του Πανεπιστημίου και ιδρυτής του Εργαστηρίου Υπηρεσιών Μετασχηματισμού, ενός εργαστηρίου δηλαδή που κάνει έρευνα στην καινοτόμα, σωστή και αποτελεσματική σχεδίαση υπηρεσιών και επιχειρηματικών διαδικασιών.
EMEAgr: Κύριε καθηγητά εξηγείστε μας, πως η μέθοδος σας και τα εργαλεία που ανέπτυξε η ερευνητική σας ομάδα, κάνει πιο εύκολη και χωρίς λάθη, την επαλήθευση κρίσιμων προγραμμάτων για την ζωή και την ασφάλεια αυτών που τα χρησιμοποιούν;
Απάντηση: Η μέθοδος του ελέγχου μοντέλων μπορεί να ανακαλύψει λάθη στο hardware (υλικό) των υπολογιστών και στα πρωτόκολλα επικοινωνίας. Η ίδια μέθοδος έχει αρχίσει να χρησιμοποιείται και για το λογισμικό (software). Για παράδειγμα, η μέθοδος ελέγχου μοντέλων θα μπορούσε να χρησιμοποιηθεί για την επαλήθευση σωστής λειτουργίας κρίσιμων προγραμμάτων ελέγχου της πτήσης ενός αεροπλάνου. Η ερευνητική μου ομάδα ελέγχει αυτόν τον καιρό την ορθότητα των προγραμμάτων ελέγχου μη επανδρωμένου αεροσκάφους που πετάει ελεύθερα χωρίς έλεγχο από το έδαφος.
EMEAgr: Πόσο πολύ έχει προχωρήσει η χρήση αυτών των μεθόδων και εργαλείων στη βιομηχανία σήμερα;
Απάντηση: Η μέθοδος ελέγχου μοντέλων χρησιμοποιείται σήμερα από εταιρείες όπως η Intel και η NEC για την επαλήθευση σχεδίων πολύπλοκων ψηφιακών κυκλωμάτων. Ένας συνάδελφός μου στα εργαστήρια JPL της NASA, ο Gerard Holzmann, έχει χρησιμοποιήσει τη μέθοδο ελέγχου μοντέλων για την επαλήθευση του λογισμικού ελέγχου του Αρειανού ρομπότ Curiosity. Και η μέθοδος λειτούργησε πολύ καλά.
EMEAgr: Είστε ικανοποιημένος από το επίπεδο χρήσης μεθόδων επαλήθευσης κρίσιμων συστημάτων υπολογιστών σήμερα;
Απάντηση: Νομίζω ότι είναι επικίνδυνο να είμαστε ποτέ ικανοποιημένοι ότι έχει ελεγχθεί πλήρως ένα κρίσιμο σύστημα (ή λογισμικό) ασφαλείας όπου εμπλέκεται ανθρώπινη ζωή. Όση επαλήθευση και να κάνουμε, ποτέ δεν θα είναι αρκετή.
EMEAgr: Είστε καθηγητής σε διάσημο πανεπιστήμιο της Αμερικής εδώ και πολλά χρόνια Θα εκτιμούσαμε ιδιαίτερα αν μας λέγατε τις σκέψεις σας για το πως βλέπετε τον ρόλο των πανεπιστημίων στο σύγχρονο κόσμο, ιδιαίτερα την χρήση της εξ αποστάσεως εκπαίδευσης. Θα αλλάξει αυτή η τεχνολογία το σύγχρονο πανεπιστήμιο; Υπάρχουν κίνδυνοι; Υπάρχουν ευκαιρίες;
Απάντηση: Νομίζω ότι η εξ’ αποστάσεως μάθηση είναι μια μεγάλη ιδέα με πολλά πιθανά οφέλη. Ωστόσο, δεν νομίζω ότι θα αντικαταστήσει ποτέ ένα πανεπιστήμιο, όπως το Carnegie Mellon, όπου οι φοιτητές μπορούν να αλληλεπιδρούν με τους διδάσκοντες των μαθημάτων τους και να κάνουν έρευνα που θα αξιολογείται από αυτούς. Επίσης, η εργαστηριακή εργασία είναι απαραίτητη για ορισμένα μαθήματα.
EMEAgr: Η Ελλάδα περνάει σήμερα μια ασυνήθιστα βαθειά οικονομική και κοινωνική κρίση. Ποιός νομίζετε ότι πρέπει να είναι ο ρόλος των πανεπιστημίων στην Ελλάδα, για το ξεπέρασμα αυτής της κρίσης;
Απάντηση: Στις ΗΠΑ, το Εθνικό Ίδρυμα Επιστημών (NSF – National Science Foundation) πιστεύει ότι η έρευνα στην Επιστήμη, Τεχνολογία, Μηχανική και τα Μαθηματικά (STEM) είναι ζωτικής σημασίας για την οικονομική ευημερία. Νομίζω ότι αυτό το είδος της έρευνας θα είναι σημαντική και στην Ελλάδα για την αντιμετώπιση της τρέχουσας οικονομικής και κοινωνικής κρίσης.
