Έλεγχος μοντέλων

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση

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

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

Σύντομη παρουσίαση[Επεξεργασία | επεξεργασία κώδικα]

Έχει αναπτυχθεί μια σημαντική κλάση μεθόδων ελέγχου μοντέλων για τον έλεγχο μοντέλων σχεδιάσεων λογισμικού και υλικού, στις οποίες οι προδιαγραφές δίνονται από μια έκφραση χρονικής λογικής. Σημαντικό έργο στον έλεγχο μοντέλων με εκφράσεις χρονικής λογικής έγινε από τους E. M. Clarke και E. A. Emerson[1][2][3] και τους J. P. Queille και Ιωσήφ Σηφάκη[4]. Ο Clarke, ο Emerson, και ο Σηφάκης μοιράστηκαν το Βραβείο Τούρινγκ το 2007 για το έργο τους στον έλεγχο μοντέλων.[5][6]

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

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

Τυπικά, το πρόβλημα μπορεί να τεθεί ως εξής: δεδομένης μιας ιδιότητας, που εκφράζεται σε χρονική λογική σαν p, και μιας δομής M με αρχική κατάσταση s, πρέπει να αποφασιστεί αν M,s \models p. Αν η M είναι πεπερασμένη, όπως στο υλικό, ο έλεγχος μοντέλων ανάγεται σε μια αναζήτηση σε γράφο.

Εργαλεία ελέγχου μοντέλων[Επεξεργασία | επεξεργασία κώδικα]

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

  1. Οι συμβολικοί αλγόριθμοι αποφεύγουν την κατασκευή του γράφου του FSM αλλά τον αναπαριστούν έμμεσα μέσω μιας έκφρασης σε προτασιακή λογική. Η χρήση διαγραμμάτων δυαδικής απόφασης (binary decision diagram, BDDs) έγινε γνωστή από το έργο του Ken McMillan.[7]
  2. Οι φραγμένοι αλγόριθμοι ελέγχου μοντέλων ξεδιπλώνουν το FSM για ένα πεπερασμένο αριθμό k βημάτων και ελέγχουν αν η παράβαση κάποιας ιδιότητας μπορεί να εμφανιστεί σε k ή λιγότερα βήματα. Αυτό συνήθως περιλαμβάνει την κωδικοποίηση του περιορισμένου μοντέλου σαν περίπτωση του προβλήματος SAT. Αυτή η διαδικασία επαναλαμβάνεται για όλο και μεγαλύτερες τιμές του k μέχρι να αποκλειστούν όλες οι πιθανές παραβάσεις (iterative deepening depth-first search).
  3. Η αναγωγή μερικής σειράς μπορεί να χρησιμοποιηθεί (σε ρητές απεικονίσεις σε γράφους) για να ελαττώσει τον αριθμό των ξεχωριστών επικαλύψεων των παράλληλων διεργασιών που αναλύονται. Η βασική ιδέα είναι ότι, αν δεν έχει σημασία αν το Α ή το Β εκτελείται πρώτο (για τα συγκεκριμένα ζητούμενα που πρέπει να αποδειχτούν), τότε δε χρειάζεται να ληφθούν υπόψη και οι δύο περιπτώσεις των επικαλύψεων ΑΒ και ΒΑ.
  4. Η αφηρημένη διερμηνεία προσπαθεί να αποδείξει ιδιότητες ενός συστήματος, απλοποιώντας το. Το απλοποιημένο σύστημα συνήθως δεν ικανοποιεί ακριβώς τις ίδιες ιδιότητες με το αυθεντικό, επομένως χρειάζεται κάποια διαδικασία επεξεργασίας της πληροφορίας. Συνήθως απαιτείται η αφαίρεση να είναι συνεπής (sound), δηλ. οι ιδιότητες που αποδεικνύονται στην αφαίρεση να ισχύουν και στο αυθεντικό σύστημα, κάποιες φορές όμως η αφαίρεση δεν είναι πλήρης (complete): δεν ισχύει ότι όλες οι ιδιότητες που ισχύουν στο αρχικό σύστημα ισχύουν και στην αφαίρεση. Ένα τέτοιο παράδειγμα είναι σε ένα πρόγραμμα να αγνοούνται οι τιμές μεταβλητών που δεν είναι τιμές αλήθειας και να λαμβάνονται υπόψη μόνο αυτές που είναι μεταβλητές αλήθειας και η ροή του ελέγχου - μια τέτοια αφαίρεση, αν και φαίνεται να πάσχει από λεπτομέρεια, μπορεί να είναι αρκετή για την απόδειξη ιδιοτήτων, π.χ. αμοιβαίου αποκλεισμού.
  5. Η εκλέπτυνση αφαίρεσης καθοδηγούμενης από αντιπαραδείγματα (counter-example guided abstraction refinement, CEGAR) αρχίζει τον έλεγχο με μια απλή (και όχι ακριβή) αφαίρεση και σταδιακά την επεξεργάζεται για μεγαλύτερη ακρίβεια. Όταν βρίσκεται μια παράβαση (αντιπαράδειγμα), το εργαλείο την αναλύει όσον αφορά την πιθανότητα εκδήλωσής της (δηλ. είναι πραγματική ή είναι αποτέλεσμα μιας λάθος αφαίρεσης;). Αν η παράβαση είναι πιθανή, αναφέρεται στο χρήστη - αν δεν είναι, η απόδειξη για αυτό χρησιμοποιείται για να βελτιωθεί η αφαίρεση και ο έλεγχος αρχίζει πάλι.[8]

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

Δείτε επίσης[Επεξεργασία | επεξεργασία κώδικα]

Εργαλεία[Επεξεργασία | επεξεργασία κώδικα]

  • ελεγκτής μοντέλων BLAST
  • CADP (Construction and Analysis of Distributed Processes) ένα σύνολο από εργαλεία για το σχεδιασμό πρωτοκόλλων επικοινωνίας και κατανεμημένων συστημάτων
  • ελεγκτής μοντέλων CHESS
  • CHIC
  • FDR2 ένας ελεγκτής μοντέλων για την επαλήθευση συστημάτων πραγματικού χρόνου με τα μοντέλα και τις προδιαγραφές σαν Επικοινωνούσες Ακολουθιακές Διεργασίες (Communicating Sequential Processes, CSP)
  • ISP επαληθευτής κώδικα για προγράμματα MPI
  • Java Pathfinder - ελεγκτής μοντέλων ανοιχτού κώδικα για προγράμματα Java
  • Markov Reward Model Checker (MRMC)
  • Εργαλεία mCRL2, Boost Software License, βασισμένα στην ACP
  • MoonWalker - ελεγκτής μοντέλων ανοιχτού κώδικα για προγράμματα .NET
  • NuSMV, ένας νέος συμβολικός ελεγκτής μοντέλων
  • PRISM (ελεγκτής μοντέλων), ένας πιθανοτικός συμβολικός ελεγκτής μοντέλων
  • Rabbit
  • Ελεγκτής μοντέλων SMART, "Symbolic Model checking Analyzer for Reliability and Timing"
  • Eλεγκτής μοντέλων SPIN, ένα γενικό εργαλείο για την επαλήθευση της ορθότητας μοντέλων κατανεμημένου λογισμικού με αυστηρό και κατά το μεγαλύτερο μέρος αυτόματο τρόπο.
  • Ελεγκτής μοντέλων TAPAs: εργαλείο για την ανάλυση της άλγερβας διεργασιών.
  • Vereofy,[9] ένας ελεγκτής μοντέλων λογισμικού για component-based systems (για λειτουργική ορθότητα)
  • μCRL, GPL, βασισμένο στην ACP
  • UPPAAL ένα περιβάλλον εργαλείων για τη μοντελοποίηση και επαλήθευση συστημάτων πραγματικού χρόνου, τα οποία έχουν μοντελοποιηθεί σαν δίκτυα χρονισμένων αυτομάτων (timed automata)

Σχετικές τεχνικές[Επεξεργασία | επεξεργασία κώδικα]

Ιστορία[Επεξεργασία | επεξεργασία κώδικα]

Παραπομπές[Επεξεργασία | επεξεργασία κώδικα]

  1. Allen Emerson, E.; Clarke, Edmund M. (1980), "Characterizing correctness properties of parallel programs using fixpoints", Automata, Languages and Programming, doi:10.1007/3-540-10003-2_69 
  2. Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic". Logic of Programs 1981: 52-71.
  3. Clarke, E. M.; Emerson, E. A.; Sistla, A. P. (1986), "Automatic verification of finite-state concurrent systems using temporal logic specifications", ACM Transactions on Programming Languages and Systems 8: 244, doi:10.1145/5397.5399 
  4. Queille, J. P.; Sifakis, J. (1982), "Specification and verification of concurrent systems in CESAR", International Symposium on Programming, doi:10.1007/3-540-11494-7_22 
  5. Press Release: ACM Turing Award Honors Founders of Automatic Verification Technology
  6. USACM: 2007 Turing Award Winners Announced
  7. * Symbolic Model Checking, Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5, also online.
  8. Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut (2000), "Counterexample-Guided Abstraction Refinement", Computer Aided Verification 1855: 154, doi:10.1007/10722167_15 
  9. Vereofy.de

Εξωτερικοί σύνδεσμοι[Επεξεργασία | επεξεργασία κώδικα]

Περαιτέρω διάβασμα[Επεξεργασία | επεξεργασία κώδικα]

Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα Model Checking της Αγγλικής Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).