Βικιπαίδεια

Έλεγχος μοντέλων: Διαφορά μεταξύ των αναθεωρήσεων

Περιήγηση ιστορικού διαδραστικά
← Προηγούμενη διαφοράΕπόμενη διαφορά →
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
ΟπτικήΚώδικας wiki
Γραμμή 40:
 
==Εργαλεία ελέγχου μοντέλων==
Τα εργαλεία ελέγχου μοντέλων αντιμετωπίζουν μια συνδυαστική έκρηξη στο χώρο των καταστάσεων, γνωστή σαν [[πρόβλημα έκρηξης καταστάσεων]], όταν πρόκειται να λύσουν πολλά από τα προβλήματα που συναντούνται στον πραγματικό κόσμο. Υπάρχουν πολλές προσεγγίσεις για την αντιετώπισηαντιμετώπιση του προβλήματος αυτού.
 
# 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 diagram]]s, (BDDs) was madeέγινε popularγνωστή byαπό theτο workέργο ofτου Ken McMillan.<ref>* ''Symbolic Model Checking'', Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5, [http://www.kenmcmil.com/thesis.html also online].</ref>
# Οι φραγμένοι αλγόριθμοι ελέγχου μοντέλων ξεδιπλώνουν το FSM για ένα πεπερασμένο αριθμό <math>k</math> βημάτων και ελέγχουν αν η παράβαση κάποιας ιδιότητας μπορεί να εμφανιστεί σε <math>k</math> ή λιγότερα βήματα. Αυτό συνήθως περιλαμβάνει την κωδικοποίηση του περιορισμένου μοντέλου σαν περίπτωση του [[πρόβλημα SAT|προβλήματος SAT]]. Αυτή η διαδικασία επαναλαμβάνεται για όλο και μεγαλύτερες τιμές του <math>k</math> μέχρι να αποκλειστούν όλες οι πιθανές παραβάσεις (iterative deepening depth-first search).
# Bounded model checking algorithms unroll the FSM for a fixed number of steps <math>k</math> and check whether a property violation can occur in <math>k</math> or fewer steps. This typically involves encoding the restricted model as an instance of [[Boolean satisfiability problem|SAT]]. The process can be repeated with larger and larger values of <math>k</math> until all possible violations have been ruled out (cf. [[Iterative deepening depth-first search]]).
# Η [[αναγωγή μερικής σειράς]] μπορεί να χρησιμοποιηθεί (σε ρητές απεικονίσεις σε γράφους) για να ελαττώσει τον αριθμό των ξεχωριστών επικαλύψεων των παράλληλων διεργασιών που αναλύονται. Η βασική ιδέα είναι ότι, αν δεν έχει σημασία αν το Α ή το Β εκτελείται πρώτο (για τα συγκεκριμένα ζητούμενα που πρέπει να αποδειχτούν), τότε δε χρειάζεται να ληφθούν υπόψη και οι δύο περιπτώσεις των επικαλύψεων ΑΒ και ΒΑ.
# [[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.
# Η [[αφηρημένη διερμηνεία]] προσπαθεί να αποδείξει ιδιότητες ενός συστήματος, απλοποιώντας το. Το απλοποιημένο σύστημα συνήθως δεν ικανοποιεί ακριβώς τις ίδιες ιδιότητες με το αυθεντικό, επομένως χρειάζεται κάποια διαδικασία επεξεργασίας της πληροφορίας. Συνήθως απαιτείται η αφαίρεση να είναι ''συνεπής'' (''sound''), δηλ. οι ιδιότητες που αποδεικνύονται στην αφαίρεση να ισχύουν και στο αυθεντικό σύστημα, κάποιες φορές όμως η αφαίρεση δεν είναι ''πλήρης'' (''complete''): δεν ισχύει ότι όλες οι ιδιότητες που ισχύουν στο αρχικό σύστημα ισχύουν και στην αφαίρεση. Ένα τέτοιο παράδειγμα είναι σε ένα πρόγραμμα να αγνοούνται οι τιμές μεταβλητών που δεν είναι τιμές αλήθειας και να λαμβάνονται υπόψη μόνο αυτές που είναι μεταβλητές αλήθειας και η ροή του ελέγχου - μια τέτοια αφαίρεση, αν και φαίνεται να πάσχει από λεπτομέρεια, μπορεί να είναι αρκετή για την απόδειξη ιδιοτήτων, π.χ. [[αμοιβαίος αποκλεισμός|αμοιβαίου αποκλεισμού]].
# [[abstract interpretation|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]].
# Η [[Εκλέπτυνση αφαίρεσης καθοδηγούμενης από αντιπαραδείγματα|εκλέπτυνση αφαίρεσης καθοδηγούμενης από αντιπαραδείγματα (counter-example guided abstraction refinement, CEGAR)]] αρχίζει τον έλεγχο με μια απλή (και όχι ακριβή) αφαίρεση και σταδιακά την επεξεργάζεται για μεγαλύτερη ακρίβεια. Όταν βρίσκεται μια παράβαση (αντιπαράδειγμα), το εργαλείο την αναλύει όσον αφορά την πιθανότητα εκδήλωσής της (δηλ. είναι πραγματική ή είναι αποτέλεσμα μιας λάθος αφαίρεσης;). Αν η παράβαση είναι πιθανή, αναφέρεται στο χρήστη - αν δεν είναι, η απόδειξη για αυτό χρησιμοποιείται για να βελτιωθεί η αφαίρεση και ο έλεγχος αρχίζει πάλι.<ref name=Clarke2000>{{citation
# [[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.<ref name=Clarke2000>{{citation
| last1 = Clarke | first1 = Edmund
| last2 = Grumberg | first2 = Orna
Ανακτήθηκε από "https://el.wikipedia.org/wiki/Έλεγχος_μοντέλων"