随机半代数混杂系统形式化分析与验证理论研究

In the fields of industrial control, aerospace, railway transportation, etc., the defects in the design of control systems may cause huge economic losses and safety accidents. The traditional formal method can perform functional verification and performance evaluation of the system by establishing functional model and performance model. However, with increasing of scale and complexity, function behaviors and performance features of the system are closely related. Many key behaviors must attached performance features to make sense. It is no longer suitable to perform functional correctness verification or performance reliability analysis independently. By implementing representation, analysis and verification of the functional behavior that attached performance features can early detect the functional errors and performance defects of the system, it is very important to ensure design correctness and performance reliability of the complex control system. In this project, we propose to investigate the hybrid analysis and verification problem of functional behavior that attached performance features and will carry out sophisticated and systematic research on embedded technology of performance features on the functional model and the representation language to construct a representation theory of the stochastic semi-algebraic hybrid system. On this basis, function and performance mixed property analysis and verification method and equivalent reduction optimization technique of the stochastic semi-algebraic hybrid system will be proposed, and will applied to the hybrid analysis and verification problem of multi-core processor control system.

在工业控制、航天航空、轨道交通等领域，调度控制系统设计的缺陷可能会造成巨大的经济损失和安全事故。传统的形式化方法通过建立功能模型和性能模型能分别对系统进行功能验证和性能评价，但随着系统规模和复杂度的增加，系统功能行为与性能指标变得密不可分，许多关键的功能行为必须附带性能指标才有意义，独立进行功能正确性验证或性能可靠性分析已不再适用，实现附带性能指标的功能行为刻画、分析与验证，尽早发现系统中的功能错误和性能缺陷，对保障复杂调度控制系统设计的正确性和性能的可靠性非常重要。本项目针对复杂调度控制系统功能行为与性能指标相结合的混合分析验证问题，着力研究系统性能指标在功能模型和性质刻画语言上的嵌入技术，建立随机半代数混杂系统表示理论，在此基础上，提出随机半代数混杂系统功能与性能混合性质分析验证方法及等价约简优化技术，并在多核处理器调度控制系统的混合分析验证问题上加以应用。

在工业控制等领域，控制系统的功能错误和性能缺陷导致的系统安全漏洞可能会造成巨大的经济损失和安全事故。随着系统规模和恶意攻击的增加，系统功能行为与性能指标变得密不可分，分别对系统进行功能验证和性能评价不能准确判定系统是否满足预期要求，许多关键的功能行为必须附带性能指标才有意义。本项目研究了控制系统性能指标在功能模型和性质刻画语言上的嵌入技术，建立了随机半代数混杂系统表示理论；提出了随机半代数混杂系统功能与性能混合性质分析验证方法及等价约简优化技术；改进了现有模糊测试技术以支撑本项目所提出方法的有效性验证。应用研究方面，将项目所提出的理论、方法和技术分别在工业控制、物联网、区块链场景下进行了应用，通过对系统、流程和业务逻辑等建立随机半代数混杂系统模型，实现了附带性能指标的功能行为刻画、分析与验证，发现系统中包括功能错误和性能缺陷在内的系统安全漏洞。针对相关研究问题，我们深入分析了国内外现有的方案，提出了自己的新方案或者改进方案，产生了包括论文、专利和软件著作权在内的相关成果。本项目的研究形成了一套随机半代数混杂系统表示及验证理论，研制出了工业控制系统建模及安全漏洞检测原型平台工具，实现了在工业控制系统安全问题上的应用。