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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Banach, R., Zhu, H.: Language evolution and healthiness for critical cyber-physical systems. J. Softw. Evol. Process. 33(9), e2301 (2021)
Jifeng, H., Qin, L.: A hybrid relational modelling language. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds.) Concurrency, Security, and Puzzles. LNCS, vol. 10160, pp. 124–143. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-51046-0_7
Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292. IEEE Computer Society (1996)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Jones, C.B.: Accommodating interference in the formal design of concurrent object-based programs. Formal Meth. Syst. Des. 8(2), 105–122 (1996). https://doi.org/10.1007/BF00122417
Lanotte, R., Merro, M., Tini, S.: A probabilistic calculus of cyber-physical systems. Inf. Comput. 279, 104618 (2021)
Lee, E.A.: Cyber physical systems: design challenges. In: ISORC, pp. 363–369. IEEE Computer Society (2008)
Li, R., Zhu, H., Banach, R.: Denotational and algebraic semantics for cyber-physical systems. In: ICECCS, pp. 123–132. IEEE (2022)
Liu, J., et al.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17164-2_1
Lunel, S., Mitsch, S., Boyer, B., Talpin, J.-P.: Parallel composition and modular verification of computer controlled systems in differential dynamic logic. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 354–370. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_22
Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319–340 (1976). https://doi.org/10.1007/BF00268134
Chaochen, Z., Ji, W., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 511–530. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0020972
Acknowledgements
This work was partly supported by the National Key Research and Development Program of China (Grant No. 2018YFB2101300), the National Natural Science Foundation of China (Grant Nos. 61872145, 62032024), Shanghai Trusted Industry Internet Software Collaborative Innovation Center, and the Dean’s Fund of Shanghai Key Laboratory of Trustworthy Computing (East China Normal University).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Li, R., Zhu, H., Banach, R. (2022). A Proof System for Cyber-Physical Systems with Shared-Variable Concurrency. In: Riesco, A., Zhang, M. (eds) Formal Methods and Software Engineering. ICFEM 2022. Lecture Notes in Computer Science, vol 13478. Springer, Cham. https://doi.org/10.1007/978-3-031-17244-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-031-17244-1_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-17243-4
Online ISBN: 978-3-031-17244-1
eBook Packages: Computer ScienceComputer Science (R0)