LTL[e] model checker Files

An LTL[e] model checker for EVENT-B model as Rodin plugins.

Brought to you by: mark2400

The interactive file manager requires Javascript. Please enable it or use sftp or scp.
You may still browse the files here.

Name	Modified	Size	InfoDownloads / Week
plugins.zip	2011-10-10	263.5 kB	0
Totals: 1 Item		263.5 kB	0

Other Useful Business Software

MongoDB Atlas runs apps anywhere

Deploy in 115+ regions with the modern database for every enterprise.

MongoDB Atlas gives you the freedom to build and run modern applications anywhere—across AWS, Azure, and Google Cloud. With global availability in over 115 regions, Atlas lets you deploy close to your users, meet compliance needs, and scale with confidence across any geography.

Start Free

$300 Free Credits to Build on Google Cloud

New customers can spin up VMs, build with AI, and query data at no cost.

Put your $300 in credit toward real workloads, then keep building with free monthly usage for 20+ products. No commitment and no charge until you upgrade.

Start Free

$300 Free Credits to Build on Google Cloud

New customers can spin up VMs, build with AI, and query data at no cost.

Put your $300 in credit toward real workloads, then keep building with free monthly usage for 20+ products. No commitment and no charge until you upgrade.

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.
Rodin
Rodin (Relational Object Dbms Implementing java binding in a Not-proprietary way) is a free implementation of Matisse, the proprietary object database. This project is still in early stage of developpement.
VanGogh Web CMS
VanGogh is our vision of a maximal flexible Content Management System (CMS). VanGogh was originally based on Rodin 1.4.6 (http://rodin.lot23.com/) but has quickly moved its focus to a more flexible design yet staying as lightweight as possible.
X-SPIN
It is a modified model checker based on SPIN to apply partial order reduction to check LTL formulae with X operator.
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).