一种面向CPS的控制应用程序协同验证方法

信息-物理融合系统是一种新型嵌入式系统计算模式，它集成了控制计算过程和受控对象，二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用，智能化程度不断提升，在具有信息物理紧密耦合特点的嵌入式系统中，嵌入式控制软件的功能比重急剧上升，作用更加突出.作为安全攸关的系统，需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.本文基于自动机理论建立统一的系统验证模型，并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求，提出了对该模型进行形式化验证的算法：基于有界模型检验方法，基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机，并基于四值语义进行判断.在求解过程中，通过偏序规约等手段化简了问题求解的规模，提高可验证系统的规模.另外结合协同仿真技术，灵活配置验证的场景，提高验证的可用性.实验结果表明，结合仿真，形式化协同验证方法可以有效地对系统进行验证.

Co-Verification Approach to Control Software Program for CPS

Cyber-Physical Systems (CPS) tightly integrate control software and plant components and transcend software and control domains.CPS are pervasive and often mission-critical, therefore, they must be high-assurance.With the extensive use of information technology, embedded control software play a greater role in such systems.The close interactions between control software and plant demand co-verification.In this paper, an automata-theoretic approach is presented to co-verification.Co-verification, verifying control software and plant together, is essential to establish the correctness of a complete system.The foundation of this approach is a unifying model for co-verification and reachability analysis of this model.We convert the LTL formula into a Büchi automata, which is interleaved with the execution of the unifying model under analysis.We propose an online-capture offline-replay approach to improve the usefulness for formal verification.Case studies on a suite of realistic examples have shown that the approach has major potential in verifying system level properties, therefore improving the high-assurance of system.