@inproceedings{99308a2f72e542c2b25f796d73dca408,
title = "A Proof System for HRML with Extended Hoare Logic",
abstract = "Hybrid systems are composed of physical components with continuous variables and discrete control components. Over time, the interacting laws of discrete and continuous dynamics manage the transition of states in hybrid systems. The operation of hybrid systems needs the combinations of computation and control. However, those combinations add the complexity of the system design and modelling. Therefore, a hybrid relational modelling language (HRML) was proposed to capture the features of hybrid systems.In this paper, we formulate a proof system for HRML to prove the correctness of hybrid systems. In our proof system, the specification and verification are based on Hoare Logic. To express the timing of observable actions, we extend the classical assertion language by adding primitives to it. Both terminating and non-terminating computations can be described in our proof system. In addition, some detailed examples are given to illustrate the application of our proof system.",
keywords = "HRML, Hoare Logic, Hybrid System, Time",
author = "Ningning Chen and Huibiao Zhu and Huixing Fang",
note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 15th International Symposium on Theoretical Aspects of Software Engineering, TASE 2021 ; Conference date: 25-08-2021 Through 27-08-2021",
year = "2021",
month = aug,
doi = "10.1109/TASE52547.2021.00017",
language = "英语",
series = "Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "31--38",
booktitle = "Proceedings - 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE 2021",
address = "美国",
}