Hybrid Rebeca Revisited

Hybrid Rebeca is introduced for modeling asynchronous event-based Cyber-Physical Systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. We provide a set of rules to define the semantic model of Hybrid Rebeca models in terms of Time Transition...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-11
Main Authors: Zhiany, Saeed, Ghassemi, Fatemeh, Abbasimoghadam, Nesa, Hodaei, Ali, Ataollahi, Ali, Kovács, József, Ábrahám, Erika, Sirjani, Marjan
Format: Article
Language:English
Subjects:
Algorithms
Cyber-physical systems
Modelling
Semantics
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Hybrid Rebeca is introduced for modeling asynchronous event-based Cyber-Physical Systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. We provide a set of rules to define the semantic model of Hybrid Rebeca models in terms of Time Transition Systems which represents an over-approximation of the reachable states of a Hybrid Rebeca model. Then, we adapt the reachability analysis algorithm of Flow\(^*\) for Hybrid Rebeca models leveraging our semantic rules. This improves the analysis significantly because the previous technique relied on the reachability analysis of hybrid automata by deriving a monolithic hybrid automaton from a given Hybrid Rebeca model, leading to a huge hybrid automaton. We illustrate the applicability of our approach through a case study.
ISSN:2331-8422