Hybrid Rebeca Revisited

TL;DR

The paper tackles safety verification of asynchronous event-based CPS with non-deterministic time by extending Hybrid Rebeca to model time intervals for delays and mode transitions. It replaces the traditional HA-transform approach with a direct Timed Transition System-based reachability analysis that adapts flowpipe construction to Hybrid Rebeca and proves its soundness. Key contributions include the time-interval extension, a direct reachability algorithm backed by formal mappings to hybrid automata, and a HyPro-enabled tool implementation with experimental results. The approach reduces intermediate model blow-up and enhances precision and scalability for complex CPS scenarios, enabling more efficient safety analysis. Practical impact lies in enabling rigorous verification of CPS where communication and computation delays are inherently non-deterministic.

Abstract

Hybrid Rebeca is a modeling framework for asynchronous event-based cyber-physical systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. Besides the syntactical extension, we formalize the semantics of the extended language in terms of Timed Transition Systems, and adapt a reachability analysis algorithm originally designed for hybrid automata to be applicable to Hybrid Rebeca models. We prove the soundness of our approach and illustrate its applicability on a case study. The case study demonstrates that our dedicated algorithm is clearly superior to the alternative approach of transforming Hybrid Rebeca models to hybrid automata as an intermediate model and then applying the original reachability analysis method to this intermediate transformed models.

Figures (8)

• Figure 1: A Hybrid Rebeca model of a room with a sensor-equipped heater, a controller, and an alarm mechanism.
• Figure 2: The monolithic hybrid automaton constructed for the Rebeca model given in Fig. \ref{['code::motiExample']}; urgent locations, in which time does not pass, are indicated by 'U'; invariants are shown in purple, guards in green, resets in blue, and the mailbox and variable values of rebecs in black.
• Figure 3: An example of an execution of a hybrid automaton and its flowpipe construction Chen.
• Figure 4: Syntax of Hybrid Rebeca. Identifiers $C$, $msg$, $\mathfrak{m}$, $v$, $c$, and $r$ denote the name of a class, message server, mode, variable, constant, and rebec, respectively.
• Figure 5: The corresponding timed transition system of the Rebeca model given in Fig. \ref{['code::motiExample']}

Theorems & Definitions (14)

• Definition 1
• Definition 2: Hybrid Rebeca model
• Definition 3: Timed Transition System for a Hybrid Rebeca model
• Definition 4: Local state of a reactive rebec
• Definition 5: State of a physical rebec
• Example 6
• Example 7
• Theorem 8
• Definition 9: Hybrid automaton for a Hybrid Rebeca model
• Definition 10: Pending event