Abstract:
The temporal logic of actions (TLA) is a logic for specifying and
reasoning about concurrent systems. Systems and their properties are
represented in the same logic, so the assertion that a system meets its
specification and the assertion that one system implements another are
both expressed by logical implication. TLA is very simple; its syntax
and complete formal semantics are summarized in about a
page. Yet, TLA is not just a logician's toy; it is extremely powerful,
both in principle and in practice. This report introduces TLA and
describes how it is used to specify and verify concurrent algorithms.
The use of TLA to specify and reason about open systems will be
described elsewhere. (51 pages)
Appeared in ACM Toplas 16, 3 (May 1994) 872-923
Postscript -
DVI
Abstract: TLA+ is a specification language for concurrent and
reactive
systems that combines the temporal logic TLA with full first-order
logic and ZF set theory. TLC is a new model checker for debugging a
TLA+ specification by checking invariance properties of a
finite-state model of the specification. It accepts a subclass of
TLA+ specifications that should include most descriptions of real
system designs. It has been used by engineers to find errors in the
cache coherence protocol for a new Compaq multiprocessor. We
describe TLA+ specifications and their TLC models, how TLC works,
and our experience using it. In Charme '99.
(12 pages)
Appeared in Correct Hardware Design and Verification Methods
(CHARME'99), Laurence Pierre and Thomas Kropf editors.
Lecture Notes in Computer Science number 1703 (1999), 54-66.
Postscript -
DVI
Abstract:
We show how to specify components of concurrent systems. The
specification of a system is the conjunction of its components'
specifications. Properties of the system are proved by reasoning
about its components. We consider both the decomposition of a given
system into parts, and the composition of given parts to form a
system.
Appeared in ACM Toplas 17, 3 (May, 1995) 507-534
Postscript -
DVI -
LaTeX
(requires acmtrans.sty)
Abstract:
Predicate-action diagrams, which are similar to conventional
state-transition diagrams, are defined as representations of formulas
in the temporal logic of actions (TLA). These diagrams can be used to
express formal properties of specifications and to illustrate
correctness proofs. (8 large pages)
Appeared in IEEE Transactions on Software Engineering 21,
9, (September 1995) 768-775
Postscript -
DVI -
LaTeX (requires
IEEEtran.sty)
There is a minor error in this paper that no-one else seems to have noticed.
Abstract:
\TLA+ is a general purpose, formal specification language based on the
Temporal Logic of Actions, with no built-in primitives for specifying
real-time properties. Here, we use \TLA+ to define operators for
specifying the temporal behavior of physical components obeying
integral equations of evolution. These operators, together with
previously defined operators for describing timing constraints, are
used to specify a toy gas burner introduced by Ravn, Rischel, and
Hansen. The burner is specified at three levels of abstraction, each
of the two lower-level specifications implementing the next
higher-level one. Correctness proofs are sketched.
Appeared in Hybrid Systems, edited by
Grossman, Nerode, Ravn, and Rischel, LNCS 736.
Postscript -
DVI -
LaTeX
Abstract:
Verifying a 64-bit multiplier has a computational complexity that puts
it beyond the grasp of current finite-state algorithms, including
those based upon homomorphic reduction, the induction principle, and
bdd fixed-point algorithms. Theorem proving, while not bound by the
same computational constraints, may not be feasible for routinely
coping with the complex, low-level details of a real multiplier. We
show how to verify such a multiplier by applying COSPAN, a
model-checking algorithm, to verify local properties of the complex
low-level circuit, and using TLP, a theorem prover based on the
Temporal Logic of Actions, to prove that these properties imply the
correctness of the multiplier. Both verification steps are automated,
and we plan to mechanize the translation between the languages of TLP
and COSPAN.
Appeared in Proceedings of the Fifth International Conference,
CAV'93. LNCS 697, 166-179.
Postscript -
DVI -
LaTeX
Abstract:
We describe an initial version of a system for mechanically checking
the correctness proof of a concurrent system. Input to the system
consists of the correctness properties, expressed in TLA (the temporal
logic of actions), and their proofs, written in a humanly readable,
hierarchically structured form. The system uses a mechanical verifier
to check each step of the proof, translating the step's assertion into
a theorem in the verifier's logic and its proof into instructions for
the verifier. Checking is now done by LP (the Larch Prover),
using two different translations--one for action reasoning and one
for temporal reasoning. The use of additional mechanical verifiers is
planned. Our immediate goal is a practical system for mechanically
checking proofs of behavioral properties of a concurrent system; we
assume ordinary properties of the data structures used by the system.
Appeared in Proceedings of the Fourth International Conference,
CAV'92. LNCS 663, 44-55.
Postscript -
DVI -
LaTeX