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).



Case Studies

Related Publications

  1. B. Yousefi, F. Ghassemi, and R. Khosravi, "Modeling and Efficient Verification of Wireless Ad hoc Networks", accepted in Formal Aspects of Computing, 2017.