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