14 lines
552 B
Text
14 lines
552 B
Text
The SMV (Symbolic Model Verifier) system is a tool for
|
|
checking finite state systems against specifications
|
|
in the temporal logic CTL (Computational Tree Logic).
|
|
|
|
One specifies the finite state system (finite automaton,
|
|
Mealy machine, full adder circuit, ..) as a Kripke
|
|
structure in the SMV language and provides specifications
|
|
in CTL. The model checking algorithm allows to determine
|
|
if the Kripke structure fulfills the specifications.
|
|
|
|
WWW: http://www-2.cs.cmu.edu/~modelcheck/smv.html
|
|
|
|
Marc E.E. van Woerkom
|
|
marc.vanwoerkom@fernuni-hagen.de
|