基于反例确认的CPS不确定性模型校准
CSTR:
作者:
作者单位:

作者简介:

杨文华(1990-),男,博士,讲师,CCF专业会员,主要研究领域为软件工程,自适应软件系统,智能软件开发.
周宇(1981-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为智能软件工程,软件演化,软件验证.
黄志球(1965-),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为软件工程,云计算,形式化方法.

通讯作者:

杨文华,E-mail:ywh@nuaa.edu.cn

中图分类号:

TP311

基金项目:

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


Calibrating Uncertainty Models for CPS Using Counterexample Validation
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61802179, 61972197); Qing Lan Project

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

杨文华,周宇,黄志球.基于反例确认的CPS不确定性模型校准.软件学报,2021,32(4):889-903

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2020-09-12
  • 最后修改日期:2020-10-26
  • 录用日期:
  • 在线发布日期: 2021-01-22
  • 出版日期: 2021-04-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号