2010 | OriginalPaper | Buchkapitel
Verifying Safety Properties with the TLA + Proof System
verfasst von : Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
Erschienen in: Automated Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
TLAPS, the TLA
+
proof system, is a platform for the development and mechanical verification of TLA
+
proofs. The TLA
+
proof language is declarative, and understanding proofs requires little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. Proofs are written in the same language as specifications; engineers do not have to translate their high-level designs into the language of a particular verification tool. A
proof manager
interprets a TLA
+
proof as a collection of
proof obligations
to be verified, which it sends to
backend verifiers
that include theorem provers, proof assistants, SMT solvers, and decision procedures.
The first public release of TLAPS is available from [1], distributed with a BSD-like license. It handles almost all the non-temporal part of TLA
+
as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties. Intuitively, a safety property asserts what is permitted to happen; a liveness property asserts what must happen; for a more formal overview, see [3,10].