Στο πρόσφατο συνέδριο της SEFI* στη Θεσσαλονίκη τιμήθηκε με το μετάλλιο Leonardo da Vinci. Ηδη, από το 2007, μαζί με τους συνεργάτες του Έντμουντ Κλάρκ και τον Έρνεστ Άλλεν Έμερσον, έχει τιμηθεί με το διεθνές βραβείο Α.Μ.Turing** για τις εργασίες τους στον έλεγχο μοντέλων (Model Checking), που αξιοποιείται πλέον από τις ΙΒΜ, Intel, Microsoft, Google και την Airbus!Ονομάζεται Ιωσήφ (Σήφης) Σηφάκης. Εργάζεται για το Εθνικό Κέντρο Επιστημονικών Ερευνών της Γαλλίας, είναι διευθυντής έρευνας στο CNRS και ιδρυτής του εργαστηρίου Verimag στη Γκρενόμπλ
...και είναι ο επιστήμονας από τον οποίο η διεθνής επιστημονική κοινότητα αναμένει την τελειοποίηση των Ενσωματωμένων Συστημάτων που θα επιτρέψουν «Το Διαδίκτυο Αντικειμένων», το «Νέο Ιντερνετ», ενδεχομένως και τη σύγκλιση νανοτεχνολογίας, πληροφορικής, γνωσιολογίας ηλεκτρονικής και μοριακής βιολογίας, «ώστε να πετύχουμε τη βελτίωση των επιδόσεων του ανθρώπου συνδυάζοντας τεχνητή και φυσική νοημοσύνη»!
* Ευρωπαϊκή Εταιρεία για την Εκπαίδευση των Μηχανικών. ** Το βραβείο Turing θεωρείται το «Νόμπελ Πληροφορικής» και από το 1956 απονέμεται κάθε χρόνο σε πρόσωπα που είχαν μια ιδιαίτερη συμβολή στη εξέλιξη της επιστήμης.
Πώς φθάσαμε στα Ενσωματωμένα Συστήματα και ποια είναι η αποστολή του Ελληνα καθηγητή
1936: θεμελιώνεται η επιστήμη της Πληροφορικής από τους Alan Turing και Kurt Goedel κυρίως για επιστημονικούς υπολογισμούς και στρατιωτικές εφαρμογές.
Δεκαετία 1970: η Πληροφορική μπαίνει στην οργάνωση και διοίκηση επιχειρήσεων, ενώ αρχίζει να αποκτά και εμπορική χρήση.
Μέσα δεκαετίας 1970: κατασκευάζονται τα πρώτα Ολοκληρωμένα Κυκλώματα.
Δεκαετία 1980: σχηματίζονται τα πρώτα Δίκτυα και αρχίζει η σύγκλιση τηλεπικοινωνιών και υπολογιστών.
Δεκαετία 1990: το Διαδίκτυο «παραδίδεται» στην ανθρωπότητα. Αρχίζει να διαμορφώνεται η «Κοινωνία της Πληροφορίας».
Δεκαετία 2000: έρχονται στη ζωή μας τα Ενσωματωμένα Συστήματα.
Η αποστολή του δρος Σηφάκη είναι, μέσω του Model Checking, να διασφαλίσει την ασφαλή και απρόσκοπτη «συνεργασία» μεταξύ διαδικτύου και Ενσωματωμένων Συστημάτων.
Τι είναι το Model Checking
«Η αρχική ιδέα ήταν να βρούμε έναν τρόπο που θα μας επιτρέπει να φτιάξουμε συστήματα ασφαλή, που δεν κάνουν λάθη όταν δουλεύουν. Συστήματα όχι για τον προσωπικό υπολογιστή αλλά για συσκευές διαφόρων ειδών, μεγάλες, όπως τα αεροπλάνα, ή μικρές, όπως τα κινητά τηλέφωνα ή οι αισθητήρες. Το ζητούμενο είναι να φτιάξουμε ασφαλή συστήματα, σε μια εμπειρική επιστήμη.
Εξ ου και το όνομα, model checking: δηλαδή μια μέθοδος επαλήθευσης που συνίστανται στην ανάπτυξη ενός μοντέλου στο οποίο μπορούμε να εξετάσουμε τις λειτουργικές προδιαγραφές (operational requirements) και να αποφασίσουμε αν το μοντέλο τις ικανοποιεί, ικανοποιεί τις ανάγκες μας.
Όταν το προτείναμε το 1981, υπήρχαν ορισμένα προβλήματα, καθώς για να γίνει η ανάλυση του μοντέλου υπήρχε πρόβλημα πολυπλοκότητας. Θα χρειαζόταν αιώνες για να εξετάσουμε όλες τις δυνατές καταστάσεις. Οπότε αναπτύξαμε τις τεχνικές που εν τέλει προτείναμε, βρήκαμε θεωρίες που μας επιτρέπουν να αναλύσουμε. Η κατάσταση των συστημάτων καθορίζει πως συμπεριφέρεται το σύστημα αμέσως μετά. Είναι η μνήμη, το παρελθόν του. Και μπορεί να έχει μεγάλο αριθμό καταστάσεων.
Ένα παράδειγμα: στον προσωπικό υπολογιστή, υπάρχει η πιθανότητα αν πατήσεις 5 τυχαία πλήκτρα και το ποντίκι μαζί, ο υπολογιστής να κολλήσει και να πρέπει να κάνεις επανέναρξη. Υπάρχουν πάρα πολλές τέτοιες καταστάσεις, που δεν ελέγχονται. Εμείς κατορθώσαμε, βρήκαμε μέθοδο για τον έλεγχο σε συστήματα μέτριας και μεσαίας πολυπλοκότητας. Η intel χρησιμοποιεί αυτή την τεχνολογία για τους επεξεργαστές της, σε κάθε επεξεργαστή χωριστά - στους πολλαπλούς είναι δύσκολος ο έλεγχος».
«Το Model Checking είναι μια τεχνική που χρησιμοποιείται σήμερα στη βιομηχανία για να επαληθεύονται τα συστήματα υπολογιστών. Αν δηλαδή τα συστήματα που φτιάχνουμε κάνουν λάθη ή όχι. Η επαλήθευση είναι πολύ σημαντική, καθώς στην Πληροφορική δεν υπάρχει ένα σύνολο γνώσεων που να επιτρέπει να κατασκευάζουμε συστήματα με προβλέψιμες ιδιότητες και συμπεριφορά. Οταν π.χ. κτίζουμε μια γέφυρα, έχουμε δοκιμασμένες θεωρίες που εγγυώνται ότι θα κρατήσει. Αυτό είναι η προβλεψιμότητα. Κάτι ανάλογο όμως δεν ισχύει στην πληροφορική.
Σήμερα πρώτα φτιάχνονται τα μεγάλα συστήματα και έπειτα βλέπουμε εάν δουλεύουν ή όχι... Αυτό που προτείναμε εμείς ήταν ένα μαθηματικό μοντέλο ελέγχου της λειτουργίας των συστημάτων που εξερευνά τις πιθανές αντιδράσεις. Οι θεωρίες επαλήθευσης είναι κρίσιμες σε μια σειρά από τομείς όπου οι πιθανές βλάβες είναι καταστροφικές, όπως στα αεροσκάφη, στα αυτοκίνητα, στις τηλεπικοινωνίες ή στα πυρηνικά εργοστάσια».
Βασικές εφαρμογές των Ενσωματωμένων Συστημάτων σήμερα:
«Οι λεγόμενες Ενσωματωμένες Τεχνολογίες χαρακτηρίζουν την εξέλιξη της πληροφορικής και αποτελούν το 98% των τσιπς, δηλαδή των Ολοκληρωμένων Συστημάτων. Εμείς βλέπουμε μόνο το 2% των τσιπς. Το 98% είναι αθέατα, καθοριστικά, όμως, για το πώς δουλεύει το κάθε αντικείμενο. Πολύπλοκα Ενσωματωμένα Συστήματα υπάρχουν κρυμμένα σε μηχανήματα, όπως αεροπλάνα, τρένα, οικιακές συσκευές, τηλέφωνα, αυτοκίνητα (ένα αυτοκίνητο μπορεί να έχει μέχρι και 80 υπολογιστές) αλλά και σε ιατρικές συσκευές (τα ρομπότ πραγματοποιούν πιο ασφαλείς επεμβάσεις)»
πηγη:goodnews.gr
