软件学报

作者：杨文华，周宇，黄志球

单位：杨文华，南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106;高安全系统的软件开发与验证技术工信部重点实验室(南京航空航天大学), 江苏 南京 211106;软件新技术与产业化协同创新中心, 江苏 南京 21009311,周宇，南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106;高安全系统的软件开发与验证技术工信部重点实验室(南京航空航天大学), 江苏 南京 21110602,黄志球，南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106;高安全系统的软件开发与验证技术工信部重点实验室(南京航空航天大学), 江苏 南京 21110603

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

基金：国家自然科学基金（61802179，61972197）；江苏省高校“青蓝工程”项目

信息物理系统被广泛应用于众多关键领域，例如工业控制与智能制造.作为部署在这些关键领域中的系统，其系统质量尤为重要.然而，由于信息物理系统自身的复杂性以及系统中存在的不确定性（例如系统通过传感器感知环境时的偏差），信息物理系统的质量保障面临巨大的挑战.验证是保障系统质量的有效途径之一，基于系统模型与规约，它可以证明系统是否满足要求的性质.现有一些信息物理系统的验证工作也取得了显著进展，例如模型检验技术就被已有工作用于验证系统在不确定性影响下的行为是否满足性质规约，并在性质违反的情况下给出具体反例.这些验证工作的一个重要输入就是不确定性模型，它描述了系统中不确定性的具体情况.而实际中要对系统中不确定性精确建模却并非易事，因此验证中使用的不确定性模型很可能与实际不完全相符，这将导致验证结果不准确并与现实偏离.针对这一问题，提出了一种基于反例确认的不确定性模型校准方法，进一步精化验证结果以提高其准确度.首先通过确认反例在系统的执行中能否被触发来判断验证使用的不确定性模型是否精确.对于不精确的模型再利用遗传算法进行校准，并根据反例确认的结果来构造遗传算法的适应度函数以指导搜索，最后结合假设检验来帮助决定是否接受校准后的结果.代表案例的实验结果表明了所提出的不确定性模型校准方法的有效性.

来源：2021年第4期

《软件学报》期刊编辑部

查看软件学报杂志2021年第4期