Verification of Hybrid Chi Model for Cyber-physical Systems Using PHAVer

Cyber-physical systems (CPSs) are integrations of computation with physical processes. CPSs are widely applied in areas such as health care, traffic control, smart home, etc. Modeling and verification of CPSs is inevitable in these areas and of the greatest challenges in CPS research. Many research reports have pointed out that developing a suitable modeling language for describing the complex system model is one of the most important challenges for CPSs. Hybrid Chi, with several features to meet the requirements of CPS modeling, is a suitable candidate. In this paper, we introduce a generalized model for CPSs, based on hybrid Chi. Through a practical example of automatic temperature control system, we show how to apply our model. Further we use Polyhedral Hybrid Automata Verifier (PHAVer) to analyze and verify the model which is simplified by a linearization algorithm. The methodology what we proposed in this paper provides a reliable foundation for the design, analysis and verification of CPSs.