Modelling and Verifying Communication Failure of Hybrid Systems in HCSP

摘要

Hybrid systems are dynamic systems with interacting discrete computation and continuous physical processes. They have become ubiquitous in our daily life, e.g. automotive, aerospace and medical systems, and in particular, many of them are safety-critical. For a safety-critical hybrid system, the physical process evolves continuously with respect to tune, and the discrete controller monitors and controls the physical process in a correct way such that the whole system satisfies the given safety requirements. The safety of hybrid systems depends heavily on the control from the controllers. However, in the presence of communication failure, the expected control from the controller will get lost and as a consequence the physical process cannot behave as expected. In this paper, we mainly consider the communication failure caused by the non-engagement of one party in communication action, i.e. the communication itself fails to occur. To address this issue, this paper proposes a formal framework by extending HCSP, a formal modeling language for hybrid systems, for modeling and verifying hybrid systems in the absence of receiving messages due to communication failure. We present two inference systems for verifying the models in the framework by leveraging the expressivity of the assertion languages and the efficiency of proofs, and correspondingly implement two theorem provers in Isabelle/HOL. To illustrate our approach, we consider a case study on train on-board control system originating from Chinese Train Control System, for which the two provers are applied separately and the proof results are compared.