Έλεγχος μοντέλων: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
μ Αντικατάσταση παρωχημένου προτύπου με references tag |
Διάσωση 3 πηγών και υποβολή 0 για αρχειοθέτηση.) #IABot (v2.0 |
||
Γραμμή 31:
| journal = International Symposium on Programming
| doi = 10.1007/3-540-11494-7_22
}}</ref>. Ο Clarke, ο Emerson, και ο Σηφάκης μοιράστηκαν το [[Βραβείο Τούρινγκ]] το 2007 για το έργο τους στον έλεγχο μοντέλων.<ref>
Ο έλεγχος μοντέλων συνήθως εφαρμόζεται σε σχεδιάσεις υλικού. Όσον αφορά το λογισμικό, λόγω της [[Υπολογισιμότητα|μη-επιλυσιμότητας]], η προσέγγιση αυτή δε μπορεί να είναι αμιγώς αλγοριθμική, στην πράξη μπορεί να αποτύχει ή να μη μπορεί να επαληθεύσει ή να διαψεύσει μια δεδομένη ιδιότητα.
Γραμμή 42:
Τα εργαλεία ελέγχου μοντέλων αντιμετωπίζουν μια συνδυαστική έκρηξη στο χώρο των καταστάσεων, γνωστή σαν [[πρόβλημα έκρηξης καταστάσεων]], όταν πρόκειται να λύσουν πολλά από τα προβλήματα που συναντούνται στον πραγματικό κόσμο. Υπάρχουν πολλές προσεγγίσεις για την αντιμετώπιση του προβλήματος αυτού.
# Οι συμβολικοί αλγόριθμοι αποφεύγουν την κατασκευή του γράφου του FSM αλλά τον αναπαριστούν έμμεσα μέσω μιας έκφρασης σε προτασιακή λογική. Η χρήση [[διάγραμμα δυαδικής απόφασης|διαγραμμάτων δυαδικής απόφασης]] (binary decision diagram, BDDs) έγινε γνωστή από το έργο του Ken McMillan.<ref>* ''Symbolic Model Checking'', Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5, [http://www.kenmcmil.com/thesis.html also online] {{Webarchive|url=https://web.archive.org/web/20070602185228/http://www.kenmcmil.com/thesis.html |date=2007-06-02 }}.</ref>
# Οι φραγμένοι αλγόριθμοι ελέγχου μοντέλων ξεδιπλώνουν το FSM για ένα πεπερασμένο αριθμό <math>k</math> βημάτων και ελέγχουν αν η παράβαση κάποιας ιδιότητας μπορεί να εμφανιστεί σε <math>k</math> ή λιγότερα βήματα. Αυτό συνήθως περιλαμβάνει την κωδικοποίηση του περιορισμένου μοντέλου σαν περίπτωση του [[πρόβλημα SAT|προβλήματος SAT]]. Αυτή η διαδικασία επαναλαμβάνεται για όλο και μεγαλύτερες τιμές του <math>k</math> μέχρι να αποκλειστούν όλες οι πιθανές παραβάσεις (iterative deepening depth-first search).
# Η [[αναγωγή μερικής σειράς]] μπορεί να χρησιμοποιηθεί (σε ρητές απεικονίσεις σε γράφους) για να ελαττώσει τον αριθμό των ξεχωριστών επικαλύψεων των παράλληλων διεργασιών που αναλύονται. Η βασική ιδέα είναι ότι, αν δεν έχει σημασία αν το Α ή το Β εκτελείται πρώτο (για τα συγκεκριμένα ζητούμενα που πρέπει να αποδειχτούν), τότε δε χρειάζεται να ληφθούν υπόψη και οι δύο περιπτώσεις των επικαλύψεων ΑΒ και ΒΑ.
Γραμμή 84:
* [[Ελεγκτής μοντέλων TAPAs]]: εργαλείο για την ανάλυση της άλγερβας διεργασιών.
* [[Vereofy]],<ref>[http://www.vereofy.de Vereofy.de]</ref> ένας ελεγκτής μοντέλων λογισμικού για component-based systems (για λειτουργική ορθότητα)
* [https://web.archive.org/web/20051127091032/http://homepages.cwi.nl/~mcrl/ μCRL], [[GNU General Public License|GPL]], βασισμένο στην [[Algebra of Communicating Processes|ACP]]
* [[Uppaal_Model_Checker | UPPAAL]] ένα περιβάλλον εργαλείων για τη μοντελοποίηση και επαλήθευση συστημάτων πραγματικού χρόνου, τα οποία έχουν μοντελοποιηθεί σαν δίκτυα χρονισμένων αυτομάτων (timed automata)
| |||