主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2022年专刊出版计划 微信服务介绍 最新一期:2021年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
杨文华,周宇,黄志球.基于反例确认的CPS不确定性模型校准.软件学报,2021,32(4):4-0
基于反例确认的CPS不确定性模型校准
Calibrating Uncertainty Models for CPS using Counterexample Validation
投稿时间:2020-09-12  修订日期:2020-10-26
DOI:10.13328/j.cnki.jos.006222
中文关键词:  信息物理系统  不确定性模型  反例确认  遗传算法
英文关键词:cyber-physical systems  uncertainty models  counterexample validation  genetic algorithms
基金项目:国家自然科学基金(61802179,61972197);江苏省高校“青蓝工程”项目;
作者单位E-mail
杨文华 南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106
高安全系统的软件开发与验证技术工信部重点实验室(南京航空航天大学), 江苏 南京 211106
软件新技术与产业化协同创新中心, 江苏 南京 210023 
ywh@nuaa.edu.cn 
周宇 南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106
高安全系统的软件开发与验证技术工信部重点实验室(南京航空航天大学), 江苏 南京 211106 
 
黄志球 南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106
高安全系统的软件开发与验证技术工信部重点实验室(南京航空航天大学), 江苏 南京 211106 
 
摘要点击次数: 163
全文下载次数: 74
中文摘要:
      信息物理系统被广泛应用于众多关键领域,例如工业控制与智能制造.作为部署在这些关键领域中的系统,其系统质量尤为重要.然而,由于信息物理系统自身的复杂性以及系统中存在的不确定性(例如系统通过传感器感知环境时的偏差),信息物理系统的质量保障面临巨大挑战.验证是保障系统质量的有效途径之一,基于系统模型与规约它可以证明系统是否满足要求的性质.现有一些信息物理系统的验证工作也取得了显著进展,例如模型检验技术就被已用工作用于验证系统在不确定性影响下的行为是否满足性质规约,并在性质违反的情况给出具体的反例.这些验证工作的一个重要输入就是不确定性模型,它描述了系统中不确定性的具体情况.而实际中要对系统中不确定性精确建模却并非易事,因此验证中使用的不确定性模型很可能与实际不完全相符,这将导致验证结果不准确并与现实偏离.针对这一问题,本文提出了一种基于反例确认的不确定性模型校准方法,来进一步精化验证结果以提高其准确度.首先通过确认反例在系统的执行中能否被触发来判断验证使用的不确定性模型是否精确.对于不精确的模型再利用遗传算法进行校准,并根据反例确认的结果来构造遗传算法的适应度函数以指导搜索,最后结合假设检验来帮助决定是否接受校准后的结果.在代表案例上的实验结果表明了我们提出的不确定性模型校准方法的有效性.
英文摘要:
      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 system quality is vital. However, due to the complexity of CPS and uncertainty in the system (such as the unpredicatable 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 paper 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 our proposed uncertainty model calibration method.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利