面向服务的信息物理融合系统建模与验证

针对信息物理融合系统(CPS)中建模与验证面临的问题与挑战,基于服务组合的思想,提出一种CPS建模与验证方法。首先,综合分析已有研究成果,提出一种CPS的组成结构,包含物理世界、感知系统、信息处理系统、控制系统及时间约束。基于该结构提出CPS资源的服务分类及组成框架,并利用时间自动机理论,提出CPS物理环境建模方法、CPS原子服务建模方法及服务组合方法。最后,通过案例设计和模型检测工具Uppaal,分别对系统安全性、可达性、活性及时间约束四种类型的性质进行了相关验证。结果表明,系统通过了这些性质的验证,这也证明了面向服务的CPS建模方法的正确性。

Modeling and verification of services oriented cyber physical systems

Concerning the problems and challenges in Cyber Physical System (CPS), a new modeling and verification method of CPS was proposed based on service composition ideas. Firstly, a composition structure of CPS was proposed, including the physical world, sensor systems, information processing systems, control systems and time constraints. Based on this proposed structure, the service classification and composition framework of CPS resources were proposed. The physical environment modeling, atomic service modeling and service composition of CPS were also given based on the timed automata theory. Finally, through case design and model checking tool Uppaal, the experimental results were given to illustrate the correctness of the CPS service-oriented modeling approach, including system security, accessibility, liveness and time constraints. The results verify the above properties and the correctness of the proposed method.