信息物理融合系统模型精化方法研究

Recently, the research and development of cyber-physical systems (CPS) have become an important direction in academia and industry. Because of the mathematical stringency of formal methods, using formal models to construct the CPS systems can improve the reliability. Since the design of complex systems always require a refinement process essentially, which is consistent with the definition of refinement checking in formal methods, it is natural to apply formal refinement method to the design of CPS systems. Based on the characteristics of the CPS systems (e.g., heterogeneity, multi-integration and time-constrained), this project researches on the refinement method of CPS system models. Specifically, on the basis of the refinement relationships of different models and the communication models between heterogeneous models, the project researches on the heterogeneous models refinement method and communication models refinement models for CPS systems. Moreover, the project also researches on the state space reduction techniques for the refinement checking algorithms in order to improve the efficiency and practicability of the method. The research of the CPS system models refinement method can assure the correctness and the consistency of the critical system properties during the model refinement process. Therefore, the design of the CPS systems can be greatly enhanced and more reliable CPS systems can be created.

近年来，信息物理融合系统（简称CPS系统）已成为国内外学术界和工业界研究开发的重要方向。采用形式化模型对CPS系统建模，有利于利用形式化方法的严格性为CPS系统的可靠性提供坚实保障。由于复杂系统模型设计的精化本质，以及与形式化方法体系中精化方法定义的一致性，使得在CPS系统模型设计中使用形式化的精化方法成为自然。本项目基于CPS系统异构性、多尺度融合性、时间约束性等内在特性，研究CPS系统模型精化方法。具体来说，研究各种异构模型精化关系以及异构模型间的通信交互，在此基础上研究CPS系统异构模型精化方法和通信交互模型精化方法，此外还需研究模型精化验证算法优化方法以提高模型精化方法的效率和实用性。CPS系统模型精化方法的研究能够保障系统关键属性在模型精化过程中的正确性和一致性，从而大大提高CPS系统设计的可信性，构建更为安全可靠的CPS系统。

由于面向信息物理融合系统（CPS）的模型精化方法能够为CPS系统精化设计提供基础理论和方法，提前探知规约中的不一致性，最终形成高可信的系统规约，本项目对CPS系统模型精化过程和方法、一致性验证规则和算法以及精化算法状态空间消减技术进行了研究。主要研究内容和结果如下。.（1）CPS系统模型的精化过程与方法：本项目从形式化模型精化过程、通信与交互模型、建模方法等方面展开研究。我们对CPS系统的组合和层次化特性进行了分析，在此基础上提出了基于时间自动机的安全属性形式化分析方法；将方法应用于一个水处理系统的验证评估，包括各部分的独立运行和交互行为、攻击行为以及安全恢复机制的建模和分析；提出了一系列基于时间自动机的属性模式，从而弥补建模分析人员和模型检测工具之间的缺口。.（2）面向CPS系统的一致性验证规则和算法：本项目从面向CPS系统的时间模型和概率模型两个角度进行一致性验证规则和算法的研究。我们提出了时间自动机trace精化检测和基于zone的精化检测算法，对已有验证算法进行了拓展；提出了基于非芝诺行为的时间自动机精化检测方法，提高验证的正确性；提出了结合关注事件的时间自动机语言包含检测，提高了精化方法的实用性；提出了概率模型精化检测方法，支持CPS系统概率行为的精化分析。.（3）精化验证算法状态空间消减技术：本项目从模拟关系和反链两个思维角度对精化验证算法状态空间消减展开研究。在基于芝诺行为检查的时间自动机精化检测算法中，利用LU模拟关系消减状态空间；在时间自动机以及概率模型相关精化检测算法中，采用反链思想使得算法只需要访问部分代表性状态并保持正确性。实验结果表明，基于模拟关系或反链的方法能够大幅度提高算法性能。.我们将提出的方法集成到了用户友好的模型检测工具PAT中。实验表明，项目所提出的模型精化过程和方法能够对CPS系统进行建模、验证并得出建设性分析结果，对该领域进行了深化拓展，相关算法具备良好的性能和实用性。