基于混合π网的信息物理融合系统可信软件形式化建模与分析

Cyber-Physical Systems (CPS) are next-generation intelligent embedded systems that integrate abstract computation and physical processes, in which sensors, actuators, and embedded devices are networked to sense, monitor, and control the physical world. A CPS is coordinated, distributed, and interconnected, and depends on the synergy of computation, communication and control components. As CPS are typically used in safety-critical systems, CPS software must be dependable. Development of high-confidence software is critical to assure the safety and effectiveness of CPS, which has become an exciting and promising research area.Formal methods are indispensable approaches to developing high-confidence CPS software. However, using only one type of formal methods is typically not sufficient to completely specify and analyze the static and dynamic CPS architecture as well as CPS system behaviors. In this project, a new type of formal methods, called hybrid π-nets is presented, which integrates two complementary formalisms, namely hybrid Petri nets and π-calculus. From the perspective of multi-agent systems, we propse a CPS formal model (CPSFM) using the hybrid π-nets. CPSFM can not only support visualizing the static and dynamic CPS architecture, and specifying CPS system behaviors, but also support modeling CPS system characteristics, such as autonomy, hybrid, and adaptation. To ensure the dependability of CPS software, we will analyze the consistency of the model after its dynamic evolution, and verify the key characteristics of CPSFM using model checking techniques. Consequently, the design errors can be detected in an early software design stage and thus, the dependability of CPS software can be significantly improved. It is our belief that this work will advance both the theoretical and practical foundation on which to design and develop high-confidence CPS software.

信息物理融合系统(Cyber-Physical Systems, CPS)集成了计算、通信与控制功能，是计算进程和物理进程深度协作和有机融合的下一代智能系统。CPS主要应用于安全关键系统中，对软件可信性要求高，因此提高软件可信性已成为CPS研究的热点和难点问题。形式化方法是可信软件研究中必不可少的手段，但单一形式化方法不能全面描述和分析系统的静态、动态结构及行为。本项目结合混合Petri网和π演算，提出一种集成的形式化方法-混合π网，从理论上突破单一形式化方法的不足；从多Agent系统的角度，以混合π网为语义基础，对CPS软件静态和动态结构进行建模，描述其非功能性需求，从而建立CPS可信软件形式化模型；针对上述模型，深入研究动态演化后系统的一致性问题，利用模型检测技术验证系统关键属性的正确性，为CPS软件设计提供可信保障。本项目对促进CPS可信软件理论与技术的发展具有重要的理论和实际意义。

信息物理融合系统(Cyber-Physical Systems, CPS)集成了计算、通信与控制功能，是计算进程和物理进程深度协作和有机融合的下一代智能系统。CPS主要应用于安全关键领域，生存环境恶劣，易遭受病毒感染、攻击或恶意代码侵袭，导致CPS功能受损、性能衰退，从而引发安全事故，因此其可信性面临着严峻的挑战。.本项目针对CPS可信软件的重大应用需求和技术特征，以构建自治高效和安全可信的CPS为目标，研究和探讨了集成形式化方法、CPS可信软件形式化建模与分析、CPS软件可信性演化动力学机理和CPS应用等一系列理论和技术难题，从而为CPS的设计与开发提供理论依据和技术手段。.本项目完成的工作主要包括以下几方面：.(1)建立了一种集成的形式化建模方法混合π网。混合π网集成了混合Petri网和π演算，利用混合Petri网描述和分析系统的静态结构和动态行为，利用π演算刻画和分析系统的动态演化，并研究了π演算的混合Petri网语义。.(2)以混合π网为语义基础，建立了CPS可信软件形式化模型CPSFM。根据多Agent系统的思想，CPSFM将CPS软件抽象为计算Agent、连接Agent和配置等三个单元，并描述了Agent的加入、退出、更新和体系结构重配置等动态演化过程。为了提高Agent的重用性，研究了计算Agent的接口组装与绑定。.(3)研究了CPSFM的形式化分析与验证技术。分析了CPS中Agent内部实现与接口的兼容性，提出了演化后系统一致性分析方法，利用模型检测技术验证了模型关键属性的正确性。.(4)研究了CPS软件可信性演化非线性动力学建模。以非线性动力学理论为基础，针对三类典型情况构建了恶意软件在CPS中的传播模型，并在此基础上建立了CPS软件可信性演化动力学模型。.(5)分析了CPS软件可信性演化的动力学行为。研究了所建动力学模型中平衡点的存在性和稳定性，分析了CPS软件可信性演化过程中将会出现的分岔现象，以及分岔的性质。.(6)研究了CPS在航空航天领域中的应用。研究了航空CPS理论，利用Petri网对其可靠性进行建模，并利用网络仿真技术对其性能进行了评估；以高超声速飞行器为对象，研究了其分布式计算与控制问题。.通过本项目的研究，可以为CPS软件在设计阶段和运行阶段提供可信保障，对于丰富和发展CPS理论及其实际应用具有一定的科学意义和工程实用价值。