 |
|
|
|
 |
 |
 |
|
 |
|
 |
|
|
杨文华,周宇,黄志球.基于反例确认的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);江苏省高校“青蓝工程”项目; |
|
摘要点击次数: 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阅读器 |
|
|
|
|
|
|
 |
|
|
|
|
 |
|
 |
|
 |
|