Translating and Verifying Cyber-Physical Systems with Shared-Variable Concurrency in SpaceEx

Ran Li, Huibiao Zhu, Richard Banach

Research output: Contribution to journalArticlepeer-review

49 Downloads (Pure)


Cyber-Physical systems (CPS), combining continuous physical behavior and discrete control behavior, have been widely utilized in recent years. However, the traditional modeling languages used to specify discrete systems are no longer applicable to CPS, since CPS subsume the combination of the cyber and the physical. To address this, a modeling language for CPS with shared-variable concurrency is proposed. In this paper, we introduce an extension to the classical configuration of transitions in Structural Operational Semantics (SOS), which adds an auxiliary variable “now” to the data state. Using this configuration, we present operational semantics for this language. Then, we propose a translation strategy from this language to hybrid automata to enable efficient verification for CPS. We give the detailed translation of basic commands and compound constructs formally, and the correctness of this translation is explored as well. To demonstrate the effectiveness of our approach, we provide an example of Autonomous Emergency Braking (AEB) and carry out the corresponding verification using SpaceEx. Compared with the existing work that uses SpaceEx for formal modeling and verification, the translation strategy from programs to automata not only allows any CPS described in this language to be modeled and verified based on the proposed strategy, but also indicates the semantic foundation on which formal verification depends.

Cyber-Physical systems (CPS)Operational semanticsShared
Original languageEnglish
Article number100864
JournalInternet of Things
Early online date7 Jul 2023
Publication statusE-pub ahead of print - 7 Jul 2023


  • Cyber-Physical Systems (CPS)
  • Operational Semantics
  • Shared Variables
  • Verification
  • SpaceEx


Dive into the research topics of 'Translating and Verifying Cyber-Physical Systems with Shared-Variable Concurrency in SpaceEx'. Together they form a unique fingerprint.

Cite this