Statistical Model Checking of Cyber-Physical Systems Control Software
Author:
Affiliation:

Clc Number:

Fund Project:

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

    Cyber physical systems (CPS) typically employ real-time multitasking systems as their control software. This paper proposes an approach to formally analyzing such control software using statistical model checking of UPPAAL. The main contribution of this study is a model in timed automata which modularly describes the major components of a multitasking system. The model supports the analysis of timing-related functional properties as well as schedulability analysis, and can easily be adapted and extended for verifying different properties of various multitasking systems. A case study on an early version of the Chinese Lunar Rover control software shows that the proposed method is able to track down undesired behavior in real-world industrial CPS.

    Reference
    Related
    Cited by
Get Citation

单黎君,周兴社,王宇英,赵雷,万丽景,乔磊,陈建新.信息物理融合系统控制软件的统计模型检验.软件学报,2015,26(2):380-389

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 15,2014
  • Revised:October 31,2014
  • Adopted:
  • Online: February 06,2015
  • 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