Overview
Rebeca to Promela translator, is a tool for automatic translation of Rebeca models into Promela codes, so that the model can be verified with SPIN model checker. The tool has been developed using Java language, so it is portable and can be run on any platform that has a Java Runtime Environment support. Current version of this tool support the following features in Rebeca model:
- Reactive Classes
- Main (system description)
- Known objects
- Message Servers
- State Variables
- Boolean variable type
- Integer variable type
- Single parameter passing in Message Servers
- Non-deterministic choice
- Synchronous Messages (as rendezvous) between Rebecs (provided for extended-Rebeca)
Artifacts
Rebeca2Promela
- Version: 2.4.1
- Last Updated: June 2007
- Size: 491 KB
- Download: [zip]