Temporal logic in finite-state verification: Meaning (information, definition, explanation, facts)

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:

[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.