Modelling and Verifying Communication Failure of Hybrid Systems in HCSP

Research output: Contribution to journalJournal article – Annual report year: 2017Researchpeer-review

Documents

DOI

View graph of relations

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 time, 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.
Original languageEnglish
JournalComputer Journal
Volume60
Issue number8
Pages (from-to)1111-1130
ISSN0010-4620
DOIs
Publication statusPublished - 2016
CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

  • Hybrid systems, HCSP, Communication failure, Safety, Inference system, Interactive theorem proving

Download statistics

No data available

ID: 134976232