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 Tomb (talk | contribs) at 03:49, 11 April 2004 (=See Also=). 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.

Property specifications are often written as Linear Temporal Logic (LTL) expressions. Once a requirement is expressed as 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.