Χρονική λογική και επαλήθευση πεπερασμένων καταστάσεων
Στην επαλήθευση πεπερασμένων καταστάσεων, οι ελεγκτές μοντέλων εξετάζουν για μηχανές πεπερασμένων καταστάσεων, που απεικονίζουν ταυτόχρονα συστήματα λογισμικού, για σφάλματα στη σχεδίασή τους. Τα σφάλμα ορίζονται σαν παραβάσεις των απαιτήσεων που έχουν εκφραστεί σαν ιδιότητες του συστήματος. Αν μια μηχανή πεπερασμένων καταστάσεων δεν ικανοποιεί κάποια ιδιότητα, ο ελεγκτής μοντέλων ίσως να είναι σε θέση να παράγει ένα αντιπαράδειγμα – μη εκτέλεση του συστήματος που δείχνει πώς συμβαίνει το σφάλμα.
Οι προδιαγραφές ιδιοτήτων συχνά γράφονται σαν εκφράσεις γραμμικής χρονικής λογικής (Linear Temporal Logic, LTL). Όταν μια απαίτηση εκφράζεται σαν πρόταση LTL, ένας ελεγκτής μοντέλων μπορεί αυτόματα να επαληθεύσει αυτήν την ιδιότητα σε σχέση με το μοντέλο.
Παράδειγμα μιας τέτοιας απαίτησης για ένα σύστημα: Από τη στιγμή που ένας ανελκυστήρας καλείται από έναν όροφο μέχρι τη στιγμή που ανοίγει τις πόρτες του σε αυτόν τον όροφο, μπορεί να φτάσει σε αυτόν τον όροφο το πολύ δύο φορές.[1] Οι συγγραφείς του "Patterns in Property Specification for Finite-State Verification" μεταφράζουν αυτήν την απαίτηση στην ακόλουθη πρόταση LTL:
Δείτε επίσης Επεξεργασία
Παραπομπές Επεξεργασία
- ↑ 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.
Αναφορές Επεξεργασία
- 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–57, 1977.