Hybrid Rebeca Revisited

TL;DR

This paper extends the Hybrid Rebeca framework to model non-deterministic time behaviors in cyber-physical systems, formalizes its semantics, and adapts a reachability analysis algorithm, demonstrating improved efficiency over traditional methods.

Contribution

It introduces syntactical and semantic extensions to Hybrid Rebeca for non-deterministic timing, along with a tailored reachability analysis algorithm.

Findings

The extended semantics are sound and formally verified.

The new algorithm outperforms the traditional hybrid automata transformation approach.

Case study validates the effectiveness of the proposed method.

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.