Co-Verification Approach to Control Software Program for CPS
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61462022, 61363071); National Key Technology R&D Program of China (2014BAD10B04, 2015BAH55F04); Major Science and Technology Project of Hainan Province (ZDKJ2016015); Natural Science Foundation of Hainan Province (614232, 614220); Enterprises-Universities-Researches Integration Project of Hainan (cxy20150025); Scientific Research Staring Foundation of Hainan University (kyqd1610)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    Cyber-Physical System (CPS) tightly integrates control software and embedded components, incorporating software with control domains. CPSs are pervasive and often mission-critical, therefore, they must have high level of security. With the extensive use of information technology, embedded control software plays a greater role in such systems. The close interactions between control software and embedded components demand co-verification. In this paper, an automata-theoretic approach is presented to co-verification. Co-verification, which verifies control software and embedded components together, is essential to establish the correctness of a complete system. The foundation of this approach is a unified model for co-verification and reachability analysis of the model. The LTL formula is converted into a Büchi automata, which is interleaved with the execution of the unified model under analysis. An online-capture offline-replay approach is proposed to improve the usefulness for formal verification. Case studies on a suite of realistic examples show that the presented approach has major potential in verifying system level properties, therefore improving the high-assurance of system.

    Reference
    Related
    Cited by
Get Citation

张雨,董云卫,冯文龙,黄梦醒.一种面向CPS的控制应用程序协同验证方法.软件学报,2017,28(5):1144-1166

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 15,2016
  • Revised:September 25,2016
  • Adopted:
  • Online: January 22,2017
  • Published:
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