中文摘要：

信息物理融合系统（cyber-physical system,CPS）作为一个新的研究方向,在其研究与发展过程中遇到了众多的问题,一些关于CPS安全的问题逐渐呈现.对CPS的设计安全进行探索性研究,主要针对CPS系统各部分之间如何安全地交互进行建模,并讨论安全数据的攻击及其防御措施的有效性.以网络化水位控制系统为例,以时间自动机为形式化建模语言对系统进行建模、验证和分析.建模过程中,采用分层的安全体系结构,分别将系统的各个组成部分的工作抽象为时间自动机模型.这些模型组成一个系统,刻画出完整的CPS工作过程.最后,利用模型检测工具PAT验证系统恢复机制的有效性.

英文摘要：

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 modelchecking tool PAT,we present a verification for the effectiveness of automated recovery mechanism.