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

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.

Keywords
Cyber-Physical systems (CPS)Operational semanticsShared
variablesVerificationSpaceEx