摘要

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