Authors
Ehsan Khamespanah, Marjan Sirjani, Zeynab Sabahi Kaviani, Ramtin Khosravi, Mohammad-Javad Izadi
Publication date
2015/2/1
Journal
Science of Computer Programming
Volume
98
Pages
184-204
Publisher
Elsevier
Description
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 …
Scholar articles
E Khamespanah, M Sirjani, ZS Kaviani, R Khosravi… - Science of Computer Programming, 2015