Formal Semantics and Analysis of Timed Rebeca in Real-Time Maude

Abstract

The actor model is one of the main models for distributed computation. Timed Rebeca is a timed extension of the actor-based modeling language Rebeca. Although Rebeca is supported by a rich verification toolset, Timed Rebeca has not had an executable formal semantics, and has therefore had limited support for formal analysis. In this paper, we provide a formal semantics of Timed Rebeca in Real-Time Maude. We have automated the translation from Timed Rebeca to Real-Time Maude, allowing Timed Rebeca models to be automatically analyzed using Real-Time Maude's reachability analysis tool and timed CTL model checker. This enables a formal model-based methodology which combines the convenience of intuitive modeling in Timed Rebeca with formal verification in Real-Time Maude. We illustrate this methodology with a collision avoidance protocol for wireless networks. © Springer International Publishing Switzerland 2014.