Description
wRebeca is an actor-based modeling language, an extension of Rebeca, proposed for modeling and verification of Mobile Ad Hoc Networks (MANETs) [1]. It is supported by the tool, which efficiently generates the state spaces of models. Several techniques have been exploited to reduce the state spaces like counting abstraction (which is sound in case the underlying topology is static) , and removal of un-observable transitions (which preserves the ACTL-X properties of the original model).
Download
- .Net version (works on Windows)
- Java Version
Contributer
- Behnaz Yousefi
Case Studies
- AODVv2 - 11 (The protocol IETF draft )
- The flooding protocol
Related Publications
- B. Yousefi, F. Ghassemi, and R. Khosravi, "Modeling and Efficient Verification of Wireless Ad hoc Networks", accepted in Formal Aspects of Computing, 2017.