基于反例确认的CPS不确定性模型校准  

Calibrating Uncertainty Models for CPS Using Counterexample Validation

作　　者：杨文华 周宇[1,2] 黄志球[1,2] YANG Wen-Hua;ZHOU Yu;HUANG Zhi-Qiu(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Key Laboratory of Safety-Critical Software of Ministry of Industry and Information Technology(Nanjing University of Aeronautics and Astronautics),Nanjing 211106,China;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 210093,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106 [2]高安全系统的软件开发与验证技术工信部重点实验室(南京航空航天大学),江苏南京211106 [3]软件新技术与产业化协同创新中心,江苏南京210093

出　　处：《软件学报》2021年第4期889-903,共15页Journal of Software

基　　金：国家自然科学基金(61802179,61972197);江苏省高校“青蓝工程”项目。

摘　　要：信息物理系统被广泛应用于众多关键领域,例如工业控制与智能制造.作为部署在这些关键领域中的系统,其系统质量尤为重要.然而,由于信息物理系统自身的复杂性以及系统中存在的不确定性(例如系统通过传感器感知环境时的偏差),信息物理系统的质量保障面临巨大的挑战.验证是保障系统质量的有效途径之一,基于系统模型与规约,它可以证明系统是否满足要求的性质.现有一些信息物理系统的验证工作也取得了显著进展,例如模型检验技术就被已有工作用于验证系统在不确定性影响下的行为是否满足性质规约,并在性质违反的情况下给出具体反例.这些验证工作的一个重要输入就是不确定性模型,它描述了系统中不确定性的具体情况.而实际中要对系统中不确定性精确建模却并非易事,因此验证中使用的不确定性模型很可能与实际不完全相符,这将导致验证结果不准确并与现实偏离.针对这一问题,提出了一种基于反例确认的不确定性模型校准方法,进一步精化验证结果以提高其准确度.首先通过确认反例在系统的执行中能否被触发来判断验证使用的不确定性模型是否精确.对于不精确的模型再利用遗传算法进行校准,并根据反例确认的结果来构造遗传算法的适应度函数以指导搜索,最后结合假设检验来帮助决定是否接受校准后的结果.代表案例的实验结果表明了所提出的不确定性模型校准方法的有效性.Cyber-physics systems(CPS) are widely used in many key areas, such as industrial control and intelligent manufacturing. As a system deployed in these key areas, its quality is vital. However, due to the complexity of CPS and uncertainty in the system(such as the unpredictable sensing error of sensors used in the system), the quality assurance of CPS faces huge challenges. Verification is one of the effective ways to ensure the quality of the system. Based on the system model and specifications, verification can prove whether the system satisfies the required properties. Significant progress has also been made in the verification of CPS. For example, model checking technology has been used in existing works to verify whether the system’s behavior under the influence of uncertainty satisfies the specification, and if not satisfied a counterexample will be given. An important input to these verification methods is the uncertainty model, which specifies the uncertainty in the system. In practice, it is not easy to accurately model the uncertainty in the system. Therefore, the uncertainty model used in the verification is likely to be inconsistent with the reality, which will lead to inaccurate verification results. To address this problem, this study proposes an uncertainty model calibration method based on counterexample validation to further improve the verification result accuracy. First, it determines whether the uncertainty model used for verification is accurate by validating whether the counterexample can be triggered during the execution of the system. For inaccurate models, the genetic algorithm is used for calibration, and the fitness function of the genetic algorithm is constructed based on the results of the counterexample validation to guide the search. Finally, hypothesis testing is used to help decide whether to accept the calibrated models. Experimental results on representative cases demonstrate the effectiveness of the proposed uncertainty model calibration method.

关 键 词：信息物理系统 不确定性模型 反例确认 遗传算法 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]