Temporal logic in finite-state verification
||This article is written like a personal reflection or opinion essay that states the Wikipedia editor's personal feelings about a topic, rather than the opinions of experts. (January 2011) (Learn how and when to remove this template message)|
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. The authors of "Patterns in Property Specification for Finite-State Verification" translate this requirement into the following LTL formula:
- Finite-state machines
- Formal methods
- Formal verification
- Kripke structure
- Linear temporal logic
- Model checking
- Temporal logic
- Dwyer, M.; Avruin, G.; Corbett, J. (March 1998). Ardis, M., ed. Patterns in Property Specification for Finite-State Verification (PDF). Proceedings of the Second Workshop on Formal Methods in Software Practice. pp. 7–15.