关键词: 时间自动机, 形式化方法, 信息物理融合系统(CPS), 安全, 验证, 建模

Abstract: Cyber-physical system (CPS), as a new research direction, has encountered a lot problems in the research and development. There are some problems about CPS security gradually appeared. In this paper, the design safety of CPS is explored. We mainly make a model on the safe interaction between the various parts of the CPS and discuss the security data attacks and the effectiveness of its defense measures. In this paper, we use the network water level control system as an example, and timed automata as formal modeling language for modeling, validating and analysing. In the process of modeling, we utilize a layered safety architecture. The work of each component of the system is respectively abstracted as a timed automata model. Those models constitute a system which describe the complete work process of CPS. Finally, by using the model-checking tool PAT, we present a verification for the effectiveness of automated recovery mechanism.

Key words: timed automata, formal method, cyber-physical system, safety, verification, modeling