@inproceedings{7d28a06d5e2048d6aadfafc83451a737,
title = "A Proof System for Cyber-Physical Systems with Shared-Variable Concurrency",
abstract = "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 verification 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 specification 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), Hoare logic, Shared variables, Trace model",
author = "Ran Li and Huibiao Zhu and Richard Banach",
note = "Publisher Copyright: {\textcopyright} 2022, Springer Nature Switzerland AG.; 23rd International Conference on Formal Engineering Methods, ICFEM 2022 ; Conference date: 24-10-2022 Through 27-10-2022",
year = "2022",
doi = "10.1007/978-3-031-17244-1\_15",
language = "英语",
isbn = "9783031172434",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "244--262",
editor = "Adrian Riesco and Min Zhang",
booktitle = "Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Proceedings",
address = "德国",
}