Hybrid Rebeca: Modeling and Analyzing of Cyber-Physical Systems

TL;DR

Hybrid Rebeca addresses the challenge of modeling and verifying cyber-physical systems with heterogeneous discrete and continuous behaviors and networked communication. It introduces Hybrid Rebeca, an actor-based language that separates software and physical actors and models the network as an explicit CAN/Wire entity, with semantics grounded in hybrid automata. A tool translates Hybrid Rebeca models into hybrid automata for formal verification with SpaceEx, demonstrated on a Brake-by-Wire ABS case study. Results show the approach can verify safety properties, with significant reduction in automaton size after aggregation, supporting scalable CPS analysis.

Abstract

In cyber-physical systems like automotive systems, there are components like sensors, actuators, and controllers that communicate asynchronously with each other. The computational model of actor supports modeling distributed asynchronously communicating systems. We propose Hybrid Rebeca language to support modeling of cyber-physical systems. Hybrid Rebeca is an extension of actor-based language Rebeca. In this extension, physical actors are introduced as new computational entities to encapsulate physical behaviors. To support various means of communication among the entities, the network is explicitly modeled as a separate entity from actors. We derive hybrid automata as the basis for analysis of Hybrid Rebeca models. We demonstrate the applicability of our approach through a case study in the domain of automotive systems. We use SpaceEx framework for the analysis of the case study.

Figures (5)

• Figure 1: A hybrid automaton for a heater which consists of two locations (modes) named on and off. Each location defines a flow and an invariant on the variable t which is the temperature. The mode of the heater changes by means of guarded transitions between the locations. The initial location is off and the initial value of t is $20$.
• Figure 2: Hybrid Rebeca model: each actor has its own thread of control, message queue, and ID. In addition to these, physical actors have modes that are defined by a guard, an invariant, and actions. Actors can communicate with each other either by sending messages through CAN or directly by wire.
• Figure 3: Abstract syntax of Hybrid Rebeca. The main differences in syntax compared to Timed Rebeca, are highlighted with color green. Angle brackets $\langle~\rangle$ denotes meta parenthesis, superscripts $+$ and $*$ respectively are used for repetition of one or more and repetition of zero or more times. Combination of $\langle~\rangle$ with repetition is used for comma separated list. Brackets $[~]$ are used for optional syntax. Identifiers $C$, $T$, $m$, $\mathfrak{m}$, $v$, $c$, $r$ and $e$ respectively denote class, primitive type, method name, mode name, variable, constant, and rebec name, respectively; and $e$ denotes an expression.
• Figure 4: The schematic of the BBW system. The physical components are shown as ellipses and computational components are shown as rectangles.
• Figure 5: The model definition of the BBW model.

Theorems & Definitions (7)

• definition thmcounterdefinition: Hybrid Rebeca model
• definition thmcounterdefinition: Message
• definition thmcounterdefinition: Hybrid automaton for Hybrid Rebeca model
• definition thmcounterdefinition: State of a rebec
• definition thmcounterdefinition: State of network
• definition thmcounterdefinition: Pending event
• definition thmcounterdefinition: Urgent location flow and invariant