SMV The SMV system is a tool for checking finite state systems against specifications in the temporal logic CTL. The input language of SMV is designed to allow the description of finite state systems that range from completely synchronous to completely asynchronous, and from the detailed to the abstract. One can readily specify a system as a synchronous Mealy machine, or as an asychronous network of abstract, nondeterministic processes. The language provides for the modular hierachical descriptions, and for the definition of reusable components.

Current Version:   2.5.3.1 License Type:   ??

Home Site: http://www.cs.cmu.edu/~modelcheck/smv.html Source Code Availability:   Yes Available Binary Packages: Debian Package:   No RedHat RPM Package:   No Other Packages:   Yes Targeted Platforms: SPARC (SunOS4, SunOS5/Solaris), Linux/ix86, Ultrix Software/Hardware Requirements: None

Other Links: None Mailing Lists/USENET News Groups: None User Comments: None See A Screen Shot? (Not Yet)

  SAL Home   |   Other Scientific Fields   |   Misc