Προβολή πηγαίου κώδικα για τη σελίδα Χρονική λογική και επαλήθευση πεπερασμένων καταστάσεων

Στην επαλήθευση πεπερασμένων καταστάσεων, οι [[έλεγχος μοντέλων|ελεγκτές μοντέλων]] εξετάζουν για [[μηχανή πεπερασμένων καταστάσεων|μηχανές πεπερασμένων καταστάσεων]], που απεικονίζουν ταυτόχρονα συστήματα λογισμικού, για σφάλματα στη σχεδίασή τους. Τα σφάλμα ορίζονται σαν παραβάσεις των απαιτήσεων που έχουν εκφραστεί σαν ιδιότητες του συστήματος. Αν μια μηχανή πεπερασμένων καταστάσεων δεν ικανοποιεί κάποια ιδιότητα, ο ελεγκτής μοντέλων ίσως να είναι σε θέση να παράγει ένα αντιπαράδειγμα &ndash; μη εκτέλεση του συστήματος που δείχνει πώς συμβαίνει το σφάλμα.

Οι προδιαγραφές ιδιοτήτων συχνά γράφονται σαν εκφράσεις [[γραμμική χρονική λογική|γραμμικής χρονικής λογικής]] (Linear Temporal Logic, LTL). Όταν μια απαίτηση εκφράζεται σαν πρόταση LTL, ένας ελεγκτής μοντέλων μπορεί αυτόματα να επαληθεύσει αυτήν την ιδιότητα σε σχέση με το μοντέλο.

Παράδειγμα μιας τέτοιας απαίτησης για ένα σύστημα:  
''Από τη στιγμή που ένας ανελκυστήρας καλείται από έναν όροφο μέχρι τη στιγμή που ανοίγει τις πόρτες του σε αυτόν τον όροφο, μπορεί να φτάσει σε αυτόν τον όροφο το πολύ δύο φορές''.<ref>M. Dwyer, G. Avruin, J. Corbett, Y. Hu, "Patterns in Property Specification for Finite-State Verification." In M. Ardis, editor, ''Proceedings of the Second Workshop on Formal Methods in Software Practice'', pages 7–15, March 1998.</ref> Οι συγγραφείς του "Patterns in Property Specification for Finite-State Verification" μεταφράζουν αυτήν την απαίτηση στην ακόλουθη πρόταση LTL:

{|
|-
|<math>\Box((call \lor \Diamond open) \to</math>
|-
|<math>((\lnot atfloor \lor \lnot open) ~\mathcal{U}</math>
|-
|<math>(open \lor ((atfloor \land \lnot open) ~\mathcal{U}</math>
|-
|<math>(open \lor ((\lnot atfloor \land \lnot open) ~\mathcal{U}</math>
|-
|<math>(open \lor ((atfloor \land \lnot open) ~\mathcal{U}</math>
|-
|<math>(open \lor (\lnot atfloor ~\mathcal{U}~ open)))))))))))</math>
|}

== Δείτε επίσης ==
*[[Μηχανή πεπερασμένων καταστάσεων]]
*[[Τυπικές μέθοδοι]]
*[[Τυπική επαλήθευση]]
*[[Δομή Κρίπκε]]
*[[Γραμμική χρονική λογική]]
*[[Έλεγχος μοντέλων]]
*[[Χρονική λογική]]

== Παραπομπές ==
<references/>

== Αναφορές ==
# Z. Manna and Amir Pnueli, ''The Temporal Logic of Reactive and Concurrent Systems: Specification'', Springer-Verlag, New York, 1991.
# Amir Pnueli, The Temporal Logic of Programs. In ''Proceedings of the 18th IEEE Symposium on Foundations of Computer Science (FOCS 1977)'', pages 46&ndash;57, 1977.

[[Κατηγορία:Τυπικές μέθοδοι]]
[[Κατηγορία:Χρονική λογική]]