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

Ship Agents Faster

Transform your applications and workflows into powerful agentic systems at global scale.

Gemini Enterprise Agent Platform lets you rapidly build, scale, govern and optimize production-ready agents grounded in your organization's data. The platform enables developers to build custom or pre-built agents for virtually any use case. New customers get $300 in free credits.

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

Ship Agents Faster

Transform your applications and workflows into powerful agentic systems at global scale.

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).