文献类型：会议论文

英文题名：Verification of Hybrid Chi Model for Cyber-Physical Systems Using PHAVer

作者：Cong Xinyu[1];Yu Huiqun[1];Xu Xin[1]

机构：[1]E China Univ Sci & Technol, Dept Comp Sci & Engn, Shanghai 200237, Peoples R China

会议论文集：7th International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing (IMIS)

会议日期：JUL 03-05, 2013

会议地点：Asia Univ, Taichung, TAIWAN

主办单位：Asia Univ

语种：英文

外文关键词：Cyber-physical systems; Hybrid Chi; modeling; verification; 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 that we proposed in this paper provides a reliable foundation for the design, analysis and verification of CPSs.