A Proof System for Cyber-physical Systems with Shared-Variable Concurrency

Ran Li, Huibiao Zhu, Richard Banach

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


Cyber-physical system (CPS) is about the interplay of discrete behaviors and continuous behaviors. The combination of the physical and the cyber may cause hardship for the modeling and verication of CPS. Hence, a language based on shared variables was proposed to realize the interaction in CPS. In this paper, we formulate a proof system for this language. To handle the parallel composition with shared variables, we extend classical Hoare triples and bring the trace model into our proof system. The introduction of the trace may complicate our
specication slightly, but it can realize a compositional proof when the program is executing. Meanwhile, this introduction can set up a bridge between our proof system and denotational semantics. Throughout this paper, we also present some examples to illustrate the usage of our proof system intuitively.

Keywords: Cyber-physical System (CPS) · Shared Variables · Trace Model · Hoare Logic.
Original languageEnglish
Title of host publication23rd International Conference on Formal Engineering Methods October 24-27, 2022, Madrid, Spain
Publication statusAccepted/In press - 23 Jun 2022


Dive into the research topics of 'A Proof System for Cyber-physical Systems with Shared-Variable Concurrency'. Together they form a unique fingerprint.

Cite this