In this paper we review the actor-based language, Timed Rebeca, with a focus on its formal semantics and formal verification techniques. Timed Rebeca can be used to model systems consisting of encapsulated components which communicate by asynchronous message passing. Messages are put in the message buffer of the receiver actor and can be seen as events. Components react to these messages/events and execute the corresponding message/event handler. Real-time features, like computation delay, network delay and periodic behavior, can be modeled in the language. We explain how both Floating-Time Transition System (FTTS) and common Timed Transition System (TTS) can be used as the semantics of such models and the basis for model checking. We use FTTS when we are interested in event-based properties, and it helps in state space reduction. For checking the properties based on the value of variables at certain point in time, we use the TTS semantics. The model checking toolset supports schedulability analysis, deadlock and queue-overflow check, and assertion based verification of Timed Rebeca models. TCTL model checking based on TTS is also possible but is not integrated in the tool.

翻译：本文综述了基于角色的语言Timed Rebeca，重点介绍其形式语义和形式化验证技术。Timed Rebeca可用于建模由封装组件构成的系统，这些组件通过异步消息传递进行通信。消息被放入接收者角色的消息缓冲区中，可视为事件。组件响应这些消息/事件并执行相应的消息/事件处理程序。该语言能够建模实时特性，如计算延迟、网络延迟和周期性行为。我们阐述了浮动时间迁移系统（FTTS）和常规时间迁移系统（TTS）如何作为此类模型的语义基础并用于模型检测。当关注基于事件的属性时，我们采用FTTS，这有助于状态空间约简。而在检测基于特定时间点上变量值的属性时，我们使用TTS语义。该模型检测工具集支持Timed Rebeca模型的调度分析、死锁与队列溢出检测以及基于断言的验证。基于TTS的TCTL模型检测虽可实现，但尚未集成至该工具中。