Temporal logic in finite-state verification

From HandWiki

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.

Example

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:[1]

[math]\displaystyle{ \begin{align}\Box((call \lor \Diamond open) \to & ((\lnot atfloor \lor \lnot open) ~\mathcal{U} \\ & (open \lor ((atfloor \land \lnot open) ~\mathcal{U}\\ & (open \lor ((\lnot atfloor \land \lnot open) ~\mathcal{U} \\ & (open \lor ((atfloor \land \lnot open) ~\mathcal{U} \\ & (open \lor (\lnot atfloor ~\mathcal{U}~ open)))))))))))\end{align} }[/math]


See also

References

  1. Dwyer, M.; Avruin, G.; Corbett, J. (March 1998). "Patterns in Property Specification for Finite-State Verification". in Ardis, M.. Proceedings of the Second Workshop on Formal Methods in Software Practice. pp. 7–15. http://santos.cis.ksu.edu/esscass04/papers/patterns-survey.pdf. 

Bibliography

  1. Z. Manna and Amir Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York, 1991.
  2. 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.