基于单工架构的信息物理系统运行时安全性保障方法  

Runtime safety assurance methods for cyber physical systems based on simplex architecture

作　　者：王强 陈强 曹伟朋 何文锋 WANG Qiang;CHEN Qiang;CAO Weipeng;HE Wenfeng(Institute of System Engineering,Academy of Military Sciences,Beijing 100070,P.R.China;Guangdong Laboratory of Artificial Intelligence and Digital Economy(Shenzhen),Shenzhen 518107,Guangdong Province,P.R.China;College of Computer Science and Software Engineering,Shenzhen University,Shenzhen 518060,Guangdong Province,P.R.China)

机构地区：[1]军事科学院系统工程研究院,北京100070 [2]人工智能与数字经济广东省实验室(深圳),广东深圳518107 [3]深圳大学计算机与软件学院,广东深圳518060

出　　处：《深圳大学学报（理工版）》2024年第3期253-263,共11页Journal of Shenzhen University(Science and Engineering)

基　　金：国家自然科学基金资助项目(62106150)。

摘　　要：运行时安全性保障方法旨在系统运行过程中确保安全性属性得到满足.基于单工(simplex)架构的运行时安全性保障方法能够在使用复杂且安全性未经验证的控制器的情况下,为系统提供安全性保证.其基本思想是将复杂且安全性未经验证的复杂控制器与经过严格形式化验证的安全控制器相结合,前者工作在无安全风险的情况下,若检测发现系统存在潜在的安全风险,则通过决策模块完成复杂控制器与安全控制器之间的切换,从而确保系统的安全性.本文重点关注基于simplex架构的信息物理系统运行时安全性保障方法,从simplex架构决策模块的设计、改进与拓展,以及simplex架构的应用3个方面展开研究,对相关工作进行了梳理和总结,指出当前面临的技术挑战,并展望未来的发展方向,认为基于simplex架构的运行时安全性保障方法将会是解决智能信息物理系统安全性保障问题的有效途径之一.Runtime safety assurance is a method that can ensure security attributes being satisfied during system operation.The simplex architecture-based runtime safety assurance methods are able to provide the safety guarantees even in the presence of unverified complex controllers.The basic idea is to combine the complex controller with a rigorously formalized safe controller,where the former operates in the absence of safety risk.Whenever a potential safety risk is detected,a decision module then completes the switching between the complex controller and the safe controller in order to guarantee the safety.This paper investigates the runtime safety assurance methods for cyber physical systems and summarizes the most relevant work from three aspects:the design of simplex decision-making module,the extension and improvement of simplex architecture,and the application of simplex architecture.This paper also provides an analysis of technical challenges and future directions of simplex architecture-based runtime safety assurance methods,indicating their potential and effectiveness in solving the runtime safety assurance issues in intelligent cyber-physical systems.

关 键 词：人工智能 形式化方法 运行时安全性保障 运行时验证 形式化建模与验证 信息物理系统 系统建模与验证 嵌入式系统 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]