Temporal logic in finite-state verification
- 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". [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, March 1998.] The authors of "Patterns in Property Specification for Finite-State Verification" translate this requirement into the following LTL formula:
See also
*Finite-state machines
*Formal methods
*Formal verification
*Kripke structure
*Linear temporal logic
*Model checking
*Temporal logic
References
[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.
Wikimedia Foundation.
2010.
Look at other dictionaries:
Temporal logic — In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a particular modal logic… … Wikipedia
Linear temporal logic — (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true,… … Wikipedia
Dynamic logic (modal logic) — For the subject in digital electronics also known as clocked logic, see dynamic logic (digital electronics). Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs and later applied to more general… … Wikipedia
Formal verification — In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods… … Wikipedia
Interval temporal logic — (also interval logic) is a temporal logic for representing both propositional and first order logical reasoning about periods of time that is capable of handling both sequential and parallel composition. Instead of dealing with infinite sequences … Wikipedia
logic, history of — Introduction the history of the discipline from its origins among the ancient Greeks to the present time. Origins of logic in the West Precursors of ancient logic There was a medieval tradition according to which the Greek philosopher … Universalium
Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… … Wikipedia
Computation tree logic — Computation tree logic (CTL) is a branching time logic, meaning that its model of time is a tree like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is… … Wikipedia
First-order logic — is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic (a less… … Wikipedia
Mathematical logic — (also known as symbolic logic) is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic.[1] The field includes both the mathematical study of logic and the… … Wikipedia
