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

Clc Number:

TP311

Fund Project:

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

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 12,2020
  • Revised:October 26,2020
  • Adopted:
  • Online: January 22,2021
  • Published: April 06,2021
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063