Next: Metatools.
Up: Tools
Previous: Proof-Oriented Tools.
These
provide implementations of one or more of the
verification algorithms discussed above. The chief virtue of these tools is
that they are automatic; the disadvantage is that the classes of system that
may be analyzed are restricted to those having some appropriate finitary
representation. Sample tools include SPIN and COSPAN, which
support model checking in linear-time formalisms; the Concurrency
Workbench, FDR, AUTO and Aldébaran, which compute various
semantic relations and (in the case of the Workbench) implement branching-time
model checkers; and Xesar and SMV, which support branching-time
model checking. PEP allows the automatic analysis of Petri-net-based
systems. Other tools have been developed for verifying real-time and hybrid
systems; these include HyTech, Kronos and Uppaal. Some
algorithmic tools, such as Statemate and the Concurrency Factory,
aim at providing support for the generation of code from system models.
Scott Smolka
Thu Aug 22 10:56:53 EDT 1996