ENuSMV-1.2

Extend NuSMV

Brought to you by: nudtwr

Add a Review

Downloads: 0 This Week

Last Update: 2013-05-30

Download

Add to Preferred Sources

ENuSMV-1.2 (extends from NuSMV-2.5.4) is a model checking tool that supporting both
BDD-based and bounded model checking of
ETL employing both finite and looping acceptance automata connectives.

Project Activity

See All Activity >

Follow ENuSMV-1.2

ENuSMV-1.2 Web Site

Other Useful Business Software

Build Agents and Models on One Platform

Everything you need to build production-ready agents and models. Access 200+ Google and third-party AI models and tools.

Gemini Enterprise Agent Platform is Google Cloud's comprehensive platform for developers to build, scale, govern, and optimize agents and models. Choose from Google's most advanced models and third-party models like Anthropic's Claude Model Family.

Start Free

Rate This Project

User Reviews

Be the first to post a review of ENuSMV-1.2!

Additional Project Details

Registered

2012-08-24

Report inappropriate content

Build Agents and Models on One Platform

Everything you need to build production-ready agents and models. Access 200+ Google and third-party AI models and tools.

Start Free

Recommended Projects

Triple-A
Triple-A (Automatic Analysis with Automata) is a full-featured library for (finite) automata written in Java with two powerful analysis tools (dealing with LTL model checking and Presburger arithmetics) and a graphical user interface built around it.
Automata editor
automata editor
Finite Automata
A package for computations with finite automata (rooted tree automorphisms) for the GAP system, http://www.gap-system.org.
Safe C Library
The Safe C Library provides bound checking memory and string functions per ISO/IEC TR24731. These functions are alternative functions to the existing standard C library that promote safer, more secure programming. The ISO/IEC Programming languages — C spec, C11, now includes the bounded APIs in Appendix K, "Bounds-checking interfaces". This latest upload supports building static library, a shared library and a linux kernel module.
STPA Verifier
STPA Verifier is an Eclipse plug-in to verify the STPA safety requirements with model checker tools such as SPIN and NuSMV. The STPA-generated safety requirements are automatically transformed into formal specification in LTL (linear Temporal Logic). The STPA Verifier plug-in fetches all LTL formulae from XSTPA and allows user to load the verification model of system (Promela or SMV Model). Furthermore, STPA verifier provides a configuration view of each model checker (SPIN and NuSMV) to enable user to configure the model checker with necessary parameters. It also allows users to extract the Promela model from C-Code of the software by using the ModeX tool. The tool shows the results of each LTL formula in the table with different values (syntax error, success, failed (counterexample)and incomplete).