Jump to content

Temporal logic in finite-state verification

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by 216.254.161.117 (talk) at 04:17, 12 March 2005 (Made Pnueli's name in citations a link). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Temporal Logic In Finite-State Verification

In finite-state verification, model checkers examine finite-state machines representing concurrent software systems looking for errors in design. Errors are defined as violations of requirements expressed as properties of the system. In the event that the finite-state machine fails to satisfy the property, a model-checker is in some cases capable of producing a counterexample -- an execution of the system demonstrating how the error occurs.

Property specifications are often written as Linear Temporal Logic (LTL) expressions. Once a requirement is expressed as an LTL formula, a model checker can automatically verify this property against the model.

One example of such a system requirement: Between the time an elevator is called at a floor and the time it opens its doors at that floor, the elevator can arrive at that floor at most twice[1]. The authors of [1] translate this requirement into the following LTL formula:


File:ElevatorLTL.JPG

See Also

External Sources

[1] 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, Mar. 1998.

[2] Z. Manna and Amir Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York, 1991

[3] 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