3db2b38cff
- Update WWW on pkg-descr. - Added SHA256 on distinfo. PR: ports/88863 Submitted by: Jean Milanez Melo <jmelo@freebsdbrasil.com.br> Approved by: maintainer timeout (19 days)
15 lines
550 B
Plaintext
15 lines
550 B
Plaintext
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.cs.cmu.edu/~modelcheck/smv.html
|
|
|
|
Marc E.E. van Woerkom
|
|
marc.vanwoerkom@fernuni-hagen.de
|