Formal Modeling and Dynamic Verification for Human Cyber Physical Systems under Uncertain Environment
Author:
Affiliation:

Clc Number:

Fund Project:

National Key R&D Program of China (2019YFA0706404); National Natural Science Foundation of China (61972150); Knowledge Service Platform of Shanghai (ZF1213); Shanghai Science and Technology Committee (20ZR1416000); Shanghai Sailing Program (21YF1432900)

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

    With the development of technology, new complex systems such as human cyber-physical systems (hCPS) have become indistinguishable from social life. The cyberspace where the software system located is increasingly integrated with the physical space of people's daily life. The uncertain factors such as the dynamic environment in the physical space, the explosive growth of the spatio-temporal data, as well as the unpredictable human behavior are all compromise the security of the system. As a result of the increasing security requirements, the scale and complexity of the system are also increasing. This situation leads to a series of problems that remain unresolved. Therefore, developing intelligent and safe human cyber-physical systems under uncertain environment is becoming the inevitable challenge for the software industry. It is difficult for the human cyber-physical systems to perceive the runtime environment accurately under uncertain surroundings. The uncertain perception will lead to the system's misinterpretation, thus affecting the security of the system. It is difficult for the system designers to construct formal specifications for the human cyber-physical systems under uncertain environment. For safety-critical systems, formal specifications are the prerequisites to ensure system security. To cope with the uncertainty of the specifications, a combination of data-driven and model-driven modeling methodology is proposed, that is, the machine learning-based algorithms are used to model the environment based on spatio-temporal data. An approach is introduced to integrate machine learning method and runtime verification technology as a unified framework to ensure the safety of the human cyber-physical systems. The proposed approach is illustrated by modeling and analyzing a scenario of the interaction of an autonomous vehicle and a human-driven motorbike.

    Reference
    Related
    Cited by
Get Citation

安冬冬,刘静,陈小红,孙海英.不确定环境下hCPS系统的形式化建模与动态验证.软件学报,2021,32(7):1999-2015

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 17,2020
  • Revised:October 26,2020
  • Adopted:
  • Online: January 22,2021
  • Published: July 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