View article

Timed Rebeca is an extension of the actor-based modeling language Rebeca that supports timing features. Rebeca is purely actor-based with no shared variables and asynchronous message passing with no explicit receive. Both computation time and network delays can be modeled in Timed Rebeca. In this paper, we propose a new approach for checking schedulability and deadlock freedom of Timed Rebeca models. The key features of Timed Rebeca, asynchrony of actors and absence of shared variables, and the focus on events instead of states in the selected properties, led us to a significant reduction in the state space. In the proposed method, there is no unique time value for each state, instead of that we store the local time of each actor separately. We prove the bisimilarity of the generated transition system, called floating time transition system, and the state space generated from the original semantics of …