diff options
Diffstat (limited to 'devel/smv/pkg-descr')
| -rw-r--r-- | devel/smv/pkg-descr | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/devel/smv/pkg-descr b/devel/smv/pkg-descr new file mode 100644 index 0000000..42f263f --- /dev/null +++ b/devel/smv/pkg-descr @@ -0,0 +1,14 @@ +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 specificaations +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 |
