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

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

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

Σύντομη παρουσίαση

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

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

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

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

Εργαλεία ελέγχου μοντέλων

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

1. Symbolic algorithms avoid ever building the graph for the FSM; instead, they represent the graph implicitly using a formula in propositional logic. The use of binary decision diagrams (BDDs) was made popular by the work of Ken McMillan.
2. Bounded model checking algorithms unroll the FSM for a fixed number of steps $k$ and check whether a property violation can occur in $k$ or fewer steps. This typically involves encoding the restricted model as an instance of SAT. The process can be repeated with larger and larger values of $k$ until all possible violations have been ruled out (cf. Iterative deepening depth-first search).
3. Partial order reduction can be used (on explicitly represented graphs) to reduce the number of independent interleavings of concurrent processes that need to be considered. The basic idea is that if it does not matter, for the kind of things one intends to prove, whether A or B is executed first, then it is a waste of time to consider both the AB and the BA interleavings.
4. Abstraction attempts to prove properties on a system by first simplifying it. The simplified system usually does not satisfy exactly the same properties as the original one so that a process of refinement may be necessary. Generally, one requires the abstraction to be sound (the properties proved on the abstraction are true of the original system); however, most often, the abstraction is not complete (not all true properties of the original system are true of the abstraction). An example of abstraction is, on a program, to ignore the values of non boolean variables and to only consider boolean variables and the control flow of the program; such an abstraction, though it may appear coarse, may in fact be sufficient to prove e.g. properties of mutual exclusion.
5. Counter-example guided abstraction refinement (CEGAR) begins checking with a coarse (imprecise) abstraction and iteratively refines it. When a violation (counter-example) is found, the tool analyzes it for feasibility (i.e., is the violation genuine or the result of an incomplete abstraction?). If the violation is feasible, it is reported to the user; if it is not, the proof of infeasibility is used to refine the abstraction and checking begins again.

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

Δείτε επίσης

Εργαλεία

• ελεγκτής μοντέλων BLAST
• CADP (Construction and Analysis of Distributed Processes) ένα σύνολο από εργαλεία για το σχεδιασμό πρωτοκόλλων επικοινωνίας και κατανεμημένων συστημάτων
• ελεγκτής μοντέλων CHESS
• CHIC
• FDR2 ένας ελεγκτής μοντέλων για την επαλήθευση συστημάτων πραγματικού χρόνου με τα μοντέλα και τις προδιαγραφές σαν CSP Processes
• 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, ένας ελεγκτής μοντέλων λογισμικού για component-based systems (για λειτουργική ορθότητα)
• μCRL, GPL, βασισμένο στην ACP
• UPPAAL ένα περιβάλλον εργαλείων για τη μοντελοποίηση και επαλήθευση συστημάτων πραγματικού χρόνου, τα οποία έχουν μοντελοποιηθεί σαν δίκτυα χρονισμένων αυτομάτων (timed automata)

Σχετικές τεχνικές

• Αφηρημένη διερμηνεία
• Αυτόματη απόδειξη θεωρημάτων
• Ανάλυσης προγράμματος (πληροφορική)
• Στατική ανάλυση

Ιστορία

• E.M. Clarke: The birth of model checking
• E. Allen Emerson: The Beginning of Model Checking: A Personal Perspective (μια καλή εισαγωγή και σύνοψη του πεδίου του ελέγχου μοντέλων)
• Model Checking, Doron Peled, Patrizio Pelliccione, Paola Spoletini, Wiley Encyclopedia of Computer Science and Engineering, 2009.

Περαιτέρω διάβασμα

• Model Checking, Doron Peled, Patrizio Pelliccione, Paola Spoletini, Wiley Encyclopedia of Computer Science and Engineering, 2009.
• Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999, ISBN 0-262-03270-8.
• Systems and Software Verification: Model-Checking Techniques and Tools, B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, ISBN 3-540-41523-8
• Logic in Computer Science: Modelling and Reasoning About Systems, Michael Huth and Mark Ryan, Cambridge University Press, 2004. DOI DOI/org.
• The Spin Model Checker: Primer and Reference Manual, Gerard J. Holzmann, Addison-Wesley, ISBN 0-321-22862-6.
• Julian Bradfield and Colin Stirling, Modal logics and mu-calculi, Inf.ed.ac.uk
• Specification Patterns KSU.edu
• Property Pattern Mappings for RAFMC Inrialpes.fr
• More patterns: page 6 of Inrialpes.fr
• Müller-Olm, M., Schmidt, D.A. and Steffen, B. Model checking: a tutorial introduction. Proc. 6th Static Analysis Symposium, G. File and A. Cortesi, eds., Springer LNCS 1694, 1999, pp. 330-354.