DocumentCode :
3109547
Title :
Verification of Hybrid Chi Model for Cyber-physical Systems Using PHAVer
Author :
Cong Xinyu ; Yu Huiqun ; Xu Xin
Author_Institution :
Dept. of Comput. Sci. & Eng., East China Univ. of Sci. & Technol., Shanghai, China
fYear :
2013
fDate :
3-5 July 2013
Firstpage :
122
Lastpage :
128
Abstract :
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.
Keywords :
automata theory; formal verification; process algebra; CPS; PHAVer; automatic temperature control system; cyber-physical system; hybrid chi model; linearization algorithm; polyhedral hybrid automata verifier; Atmospheric modeling; Computational modeling; Computers; Delays; Synchronization; Temperature sensors; Cyber-physical systems; Hybrid Chi; PHAVer; modeling; verification;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Innovative Mobile and Internet Services in Ubiquitous Computing (IMIS), 2013 Seventh International Conference on
Conference_Location :
Taichung
Type :
conf
DOI :
10.1109/IMIS.2013.29
Filename :
6603660
Link To Document :
بازگشت