Τυπική επαλήθευση

Στα συστήματα υλικού και λογισμικού, η τυπική επαλήθευση (formal verification) είναι η απόδειξη της ορθότητας των αλγορίθμων ενός συστήματος σύμφωνα με κάποια τυπική προδιαγραφή ή ιδιότητα, με τη χρήση τυπικών μεθόδων των μαθηματικών.

Χρήση

Η τυπική επαλήθευση μπορεί να χρησιμεύσει στην απόδειξη της ορθότητας συστημάτων όπως τα κρυπτογραφικά πρωτόκολλα, τα συνδυαστικά κυκλώματα, τα ψηφιακά κυκλώματα με εσωτερική μνήμη και το λογισμικό με τη μορφή πηγαίου κώδικα.

Αυτά τα συστήματα επαληθεύονται μέσω κάποιας τυπικής απόδειξης σε ένα αφηρημένο μαθηματικό μοντέλο του συστήματος. Η αντιστοιχία μεταξύ του μαθηματικού μοντέλου και της φύσης του συστήματος θεωρείται ήδη γνωστή από τη διαδικασία της κατασκευής του μοντέλου. Παραδείγματα μαθηματικών αντικειμένων που χρησιμοποιούνται συχνά για τη μοντελοποίηση συστημάτων είναι οι μηχανές πεπερασμένων καταστάσεων, τα συστήματα μεταβάσεων με ετικέτες (labelled transition systems), τα δίκτυα Petri, τα χρονισμένα αυτόματα (timed automata), τα υβριδικά αυτόματα, η άλγεβρα διεργασιών (process algebra) και η τυπική σημασιολογία των γλωσσών προγραμματισμού, όπως η λειτουργική σημασιολογία, η δηλωτική σημασιολογία, η αξιωματική σημασιολογία και η λογική Χόαρ.

Τρόποι τυπικής επαλήθευσης

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

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

Οι τεχνικές υλοποίησης περιλαμβάνουν την απαρίθμηση του χώρου των καταστάσεων (state space enumeration), τη συμβολική αναπαράσταση του χώρου των καταστάσεων (symbolic state space enumeration), την αφηρημένη διερμηνεία (abstract interpretation), τη συμβολική προσοοίωση (symbolic simulation) και την αφηρημένη εκλέπτυνση (abstraction refinement). Οι ιδιότητες προς επαλήθευση συνήθως περιγράφονται σε χρονικές λογικές, όπως η γραμμική χρονική λογική (LTL) ή η λογική υπολογιστικού δένδρου (CTL).

Η δεύτερη προσέγγιση είναι η λογική επαγωγή. Χρησιμοποιεί μια τυπική μέθοδο μαθηματικής συλλογιστικής για το σύστημα, συνήθως με χρήση λογισμικού απόδειξης θεωρημάτων (πολλές φορές λογικής ανώτερης τάξης) όπως οι αποδείκτες θεωρημάτων ACL2, Agda, Isabelle και Coq.

Συνήθως πρόκειται για λογισμικό με μερικούς αυτοματισμούς, που καθοδηγείται από το χρήστη και το τι έχει κατανοήσει για το σύστημα που πρόκειται να επαληθεύσει. Κάποια εργαλεία όπως το Perfect Developer και το ArC προσπαθούν να αυτοματοποιήσουν πλήρως τη διαδικασία της απόδειξης.

Επικύρωση και επαλήθευση

Η επαλήθευση (verification) είναι η μια πλευρά του ελέγχου της ορθότητας ενός προϊόντος. Η επικύρωση (validation) είναι συμπληρωματική αυτής. Συνηθως όλη η διαδικασία ελέγχου αποκαλείται V & V.

Επικύρωση: "Προσπαθούμε όντως να κατασκευάσουμε το σωστό πράγμα;", δηλ. οι προδιαγραφές του προϊόντος συμπίπτουν με τις πραγματικές ανάγκες του χρήστη;
Επαλήθευση: "Κατασκευάσαμε αυτό που προσπαθούσαμε να κατασκευάσουμε;", δηλ. το προϊόν συμφωνεί με τις προδιαγραφές;

Η διαδικασία επαλήθευσης αποτελείται από στατικές/δομικές και δυναμικές/συμπεριφορικές όψεις. Π.χ. σε ένα προϊόν λογισμικού μπορεί κάποιος να εξετάσει τον πηγαίο κώδικα (στατικά) και να τον εκτελέσει ως προς κάποιους ελέγχους (δυναμικά). Η επικύρωση συνήθως γίνεται μόνο δυναμικά, δηλ. το προϊόν ελέγχεται σε τυπικές (και λιγότερο τυπικές) χρήσεις ("Συμφωνεί ικανοποιητικά με όλες τις περιπτώσεις χρήσης (use cases);"). Δείτε επίσης Επαλήθευση και επικύρωση.

Εμπορική χρήση

Η αύξηση της πολυπλοκότητας των σχεδιάσεων αυξάνει τη σημασία των τεχνικών τυπικής επαλήθευσης στη βιομηχανία του υλικού.^[1]^[2] Προς το παρόν, η τυπική επαλήθευση χρησιμοποιείται από τις περισσότερες εταιρείες κατασκευής υλικού, ενώ χρησιμοποιείται λιγότερο στη βιομηχανία του λογισμικού. Αυτό μπορεί να οφείλεται στη μεγαλύτερη ανάγκη της βιομηχανίας του υλικού, όπου τα λάθη έχουν μεγαλύτερη εμπορική σημασία. Λόγω των πιθανών πολύπλοκων αλληλεπιδράσεων μεταξύ των στοιχείων, είναι όλο και πιο δύσκολο να εξεταστούν ρεαλιστικά σύνολα πιθανών συμπεριφορών μέσω της προσομοίωσης. Σημαντικά θέματα της σχεδίασης υλικού προσφέρονται για αυτόματες μεθόδους απόδειξης, με την τυπική επαλήθευση να είναι πιο εύκολο να χρησιμοποιηθεί παραγωγικά.^[3]

Δύο λειτουργικά συστήματα που έχουν επαληθευτεί τυπικά είναι ο ενσωματωμένος μικροπυρήνας L4 της NICTA (Secure Embedded L4 microkernel) και το λειτουργικό σύστημα Integrity της Green Hills Software.^[4]

Δείτε επίσης

Αναφορές

[1] ttp://www2.computer.org/portal/web/csdl/doi/10.1109/LICS.2003.1210044^{[νεκρός σύνδεσμος]}

[2] ttp://portal.acm.org/citation.cfm?id=800667

[3] Formal Verification in Industry

[4] "A new OS has been proven to be correct using mathematical proofs. The cost: astronomical."^{[νεκρός σύνδεσμος]} by Jack Ganssle

[1]

[2]

[3]

[4]