Timed Actors and Their Formal Verification

TL;DR

This paper reviews the formal semantics and verification methods for Timed Rebeca, an actor-based language modeling real-time systems with asynchronous message passing, supporting various analysis techniques.

Contribution

It introduces formal semantics for Timed Rebeca using FTTS and TTS, and demonstrates its model checking capabilities for real-time system properties.

Findings

Supports schedulability, deadlock, and overflow analysis

Enables assertion-based verification of models

Facilitates event-based and variable-based property checking

Abstract

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.