An LTL[e] model checker for EVENT-B model as Rodin plugins.
There are two algorithms for detecting accepting cycle: one is based on Nested Depth First Search (NDFS), another based on Strongly Connected Components (SCCs).
Download Rodin platform from http://www.deploy-project.eu/ or eventb.org, then add this plugin for LTL[e] model checher for event-b model,(reqiures ProB library)
Features
- Formal methods
- LTL[e]
- model checking
- event-b
- plugins
Follow LTL[e] model checker
You Might Also Like
WorkforceHub is the instantly useful, delightfully simple to use, small business solution for tracking time, scheduling and hiring. It scales as your business grows while delivering the mission-critical features an organization needs. It is tailored to, built for, and priced for small business employers.
Rate This Project
Login To Rate This Project
User Reviews
Be the first to post a review of LTL[e] model checker!