X-SPIN

Brought to you by: kanshuanglong

Add a Review

Downloads: 0 This Week

Last Update: 2015-08-10

Download

Get an email when there's a new version of X-SPIN

It is a modified model checker based on SPIN to apply partial order reduction to check LTL formulae with X operator.

Project Activity

See All Activity >

Follow X-SPIN

X-SPIN 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.

Get Started Free

Rate This Project

User Reviews

Be the first to post a review of X-SPIN!

Additional Project Details

Registered

2015-08-04

Report inappropriate content

Ship Agents Faster

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

Get Started Free

Recommended Projects

Spin
Spin is a transparent threading solution for non-freezing Swing applications.
SPIN Eclipse Integration
SPIN Eclipse Integration (Plugin)
disk spin-up utility
A simple tool to keep external hardrives from spinning down
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).
LTL3BA
Translator of LTL formulae to Büchi automata based on LTL2BA