Next: Algorithmic tools.
Up: Tools
Previous: Tools
These
typically employ a theory for reasoning about
concurrent systems in conjunction with a deduction engine to allow users to
conduct proofs that systems enjoy certain properties. The virtue of such tools
is that they permit the analysis of systems---such as those that are
parameterized or manipulate data---that lie beyond the scope of fully automated
tools; their disadvantage is that they can require substantial user
interaction. Sample tools include PVS and PSF, which both enrich
type theories for manipulating values with notions of concurrency and which
have been used to prove the correctness of parameterized systems and
distributed algorithms and protocols; STeP, which provides automated
support for establishing that concurrent systems satisfy temporal formulas as
well as a decision procedure for temporal logic and a model checker; and
PAM, which oversees the construction of algebraic proofs of equivalence
between terms in a process algebra that the user specifies.
Scott Smolka
Thu Aug 22 10:56:53 EDT 1996