前瞻科技

特性	详细描述
可观察性（Observation-based）	监控器应该重点考虑原系统控制器的可观察性，而不查看在其内部（可能是模糊的）执行代码
确定性（Determinism Preservation）	RE中的防护器生成算法不应该引入非确定性
可用性（Feasibility）	防护器生成算法的复杂度应该是多项式的
避免死锁（Deadlock-freedom）	强制过程不能在被监控系统中引入死锁
避免分歧（Divergence-freedom）	强制过程不能在被监控系统中引入分歧
可扩展性（Scalability）	算法应该具备足够的可扩展性以适应原系统控制器

特性	详细描述
可观察性（Observation-based）	监控器应该重点考虑原系统控制器的可观察性，而不查看在其内部（可能是模糊的）执行代码
确定性（Determinism Preservation）	RE中的防护器生成算法不应该引入非确定性
可用性（Feasibility）	防护器生成算法的复杂度应该是多项式的
避免死锁（Deadlock-freedom）	强制过程不能在被监控系统中引入死锁
避免分歧（Divergence-freedom）	强制过程不能在被监控系统中引入分歧
可扩展性（Scalability）	算法应该具备足够的可扩展性以适应原系统控制器

软件运行时验证与监控技术发展现状与展望

PDF下载

卜磊 ¹^,² , 董威 ³^,^† , 单云霄 ⁴^,⁵

前瞻科技 | 综述与述评 2023,2(1): 62-77

收起

前瞻科技 | 综述与述评 2023, 2(1): 62-77

软件运行时验证与监控技术发展现状与展望

全屏

卜磊¹^,², 董威³^,^†, 单云霄⁴^,⁵

作者信息

1.南京大学计算机软件新技术国家重点实验室，南京 210023

2.南京大学软件学院，南京 210023

3.国防科技大学计算机学院，长沙 410073

4.中山大学人工智能学院，珠海 519082

5.广东省大数据分析与处理重点实验室，广州 510275

卜磊，教授，博士研究生导师。中国计算机学会系统软件专业委员会秘书长。主要研究领域为软件工程与形式化方法，包括模型检验技术、实时混成系统、信息物理融合系统等方向。入选国家级青年人才计划、高校计算机专业优秀教师奖励计划。获NASAC青年软件创新奖、CCF-IEEE CS青年科学家奖等。电子信箱：bulei@nju.edu.cn。

董威，教授，博士研究生导师。中国计算机学会形式化方法专业委员会秘书长。主要研究方向为高可信软件技术、智能化软件开发方法。入选教育部新世纪优秀人才支持计划。获NASAC青年软件创新奖、霍英东教育基金会高等院校青年教师奖等。先后主持国家自然科学基金重大项目、国家高技术研究发展计划、国家重点基础研究发展计划和国防领域课题10余项。出版国家级规划教材2部，发表学术论文70余篇。电子信箱：wdong@nudt.edu.cn。

通信作者:

^†

Current Status and Prospects of Runtime Software Verification and Monitoring

Lei BU¹^,², Wei DONG³^,^†, Yunxiao SHAN⁴^,⁵

Affiliations

1. State Key Laboratory for Novel Software Technology at Nanjing University, Nanjing 210023, China

2. Software Institute, Nanjing University, Nanjing 210023, China

3. College of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China

4. School of Artificial Intelligence, Sun Yat-sen University, Zhuhai 519082, China

5. Guangdong Key Laboratory of Big Data Analysis and Processing, Guangzhou 510275, China

出版时间: 2023-03-20 doi: 10.3981/j.issn.2097-0781.2023.01.005

文章导航

摘要

收起

当今社会，大量软件系统运行在开放、动态、不确定的场景中，经常受到非预期的干扰和影响，因此对系统行为进行运行时验证与监控，并针对各种实时情况做出自适应的实时响应、决策与动态调控，具有重要意义。文章从运行时验证、监控、增强及动态调控等方面对相关领域的国内外进展进行了回顾与展望，并从软件行为认知与理解、控制器生成、全生命期监控等角度对后续潜在方向进行探讨与建议。

关键词

形式化建模与验证 / 运行时验证 / 在线监控 / 控制生成

Abstract

收起

Nowadays, many software systems are working in open, dynamic, and nondeterministic scenarios, often suffering from unexpected interference and influence. It is important to conduct runtime verification and monitoring of system behavior and adaptively make real-time responses and decisions for and exert dynamic control over each real-time situation. This paper reviews the research progress of runtime verification, monitoring, enhancement, and dynamical control in and outside China and their prospects. Meanwhile, it also explores and recommends potential future research directions from the perspectives of the understanding of system behavior, controller synthesis, full-cycle monitoring, etc.

Key words

formal modeling and verification / runtime verification / online monitoring / control synthesis

引用本文

卜磊, 董威, 单云霄. 软件运行时验证与监控技术发展现状与展望. 前瞻科技, 2023 , 2 (1) : 62 -77 . DOI: 10.3981/j.issn.2097-0781.2023.01.005

Lei BU, Wei DONG, Yunxiao SHAN. Current Status and Prospects of Runtime Software Verification and Monitoring[J]. Science and Technology Foresight, 2023 , 2 (1) : 62 -77 . DOI: 10.3981/j.issn.2097-0781.2023.01.005

正文

收起

当今世界，软件已经遍布人类社会的方方面面，并在生产和生活的各个角落发挥着不可替代的重要作用。在软件能力快速提升的同时，软件的工作方式与环境也在发生巨大的变化。与传统软件系统运行在既定简单环境下，接收固定输入并按预定逻辑进行响应不同，现代软件系统大量嵌入在各类复杂系统中，运行在各种开放、动态的环境下，需要通过整合计算部件与物理环境，实时感知与捕获外界动态变化的环境数据，并根据相关环境和任务的变化，依据控制规则或者智能学习算法对软件组件间交互进行动态重构，对组件内计算逻辑进行自动调整。在此方式下，软件可以更精确地获取外界信息并做出针对性的实时反应，提高任务处理的性能与质量，从而提供及时、精确且可靠的服务。

然而，在给软件行为带来精密、高效、快捷等优势的同时，开放不确定场景也给相关软件的设计、实现与可信保障带来了巨大的挑战。以自动驾驶系统为例，其在运行中会采集实时数据来调整自身行为，而这些实时数据中包含周围行人与车辆的位置、运行方向、速度、道路中突现障碍等。这些数据在设计阶段完全无法进行准确预测与描述。在智能制造领域，相关问题同样非常突出，针对实时到达的不同订单，智能车间中的各机器人、机械臂，针对当前具体任务，以及各机器人当前位置、物料分布等情况，实时构建相互之间的组网协作与拓扑关系，并进一步进行行为决策与控制。类似的场景在列控、医疗等任务关键领域比比皆是，已然成为现代软件工作的新常态。

在开放不确定，乃至完全未知、未见的场景下，如何保障软件实时行为保持安全，保障软件实时决策的安全精准，对于系统的整体可信保障具有重要的意义，并成为近年来相关研究领域的热点关注方向。对软件系统的正确性进行检测，目前主要有3种基本手段：定理证明^[1]、模型检验^[2]和软件测试^[3]。前两种都需要对软件系统进行建模，在明确外界输入范围的情况下，定理证明采用数学推理的方式，模型检验采用状态遍历的方式对软件系统正确性进行静态验证。软件测试一般采用在一定输入条件下，对比系统输出与标准输出一致性的方法对软件可靠性进行动态检测。与以上3种方法相比，运行时验证（Runtime Verification, RV）^[4]主要对运行的软件进行实时监控，根据系统行为是否违背某些规约做出反应。与同样采用形式化方式的模型检验、定理证明相比，运行时验证具有较低的复杂度，可针对系统实时行为进行检验。而与测试相比，运行时验证在对属性进行描述和对程序的监控方面具有更好的灵活性和可扩展性。因此，面向开放不确定环境下安全攸关系统的高可信保障需求，对系统行为进行运行时验证与监控，确保系统安全，并针对各种实时情况做出基于验证的自适应实时响应、决策和动态调控，是相关领域重点关注的研究方向，并取得了一系列进展与突破。本研究将对相关领域国内外进展进行简要分析、总结，并对相关领域研究方向进行展望与讨论。

1 国外研究进展

收起

1.1 运行时监控与验证

随着计算系统变得越来越复杂，人们逐渐认识到监控的重要性，认为监控是对计算过程（例如进程）中所关心的动态信息进行抽取，并且应该与操作系统的控制管理过程或同步系统的访问仲裁过程中所出现的监控器（Monitor）概念相区分^[5]。在电气与电子工程师协会（Institute of Electrical and Electronics Engineers, IEEE）标准中，监控器被定义为“与一个系统或构件并发运行，并对系统或构件的操作进行监督、记录、分析或验证的软件工具或硬件设备”^[6]。早期监控方法主要基于跟踪和采样技术并主要用于调试、优化、状态报告、重配置等用途。因此，Snodgrass^[5]认为传统监控技术已经不适于监控具有多处理器、分布式特征的复杂系统，同时提出了基于历史数据以及包括数据收集、数据分析和结果显示等步骤的监控过程。人们普遍认为，缺乏集中控制以及在大量不同系统构件（如节点、处理器、进程、内存、地址域等）之间进行跳转是造成复杂系统监控非常困难的主要原因之一，因而构造构件级监控器对分布式系统输入输出和部分状态信息进行监控，然后通过组合技术获取全局监控信息成为一种分而治之、处理复杂性的方式^[7-8]。

监控可以针对系统和软件中的不同侧面，这与应用背景、需求以及用户的关注点相关，并已出现许多相关研究工作。例如，采用不变式或断言对软件运行过程中的变量值、输入/输出或系统状态进行监控^[9];对网络中出现的恶意攻击和非法访问进行监控^[10];以形式规约中提取的事件表达式作为基础对系统的实时性进行监控^[11];通过软件运行时监控技术对无线网络中的能耗进行监测^[12];在面向服务的体系结构（Service Oriented Architecture）中，通过软件封装（Wrapping）技术对Web服务的性能进行监控^[13]，以及针对Web服务会话研究运行时监控所需的性质模板^[4]等。

为了更准确地对复杂时序属性进行监控，以形式化方法为基础的运行时验证得到广泛重视，已被认为是运行时监控的重要研究领域。运行时验证的目标是检测一个系统的实际运行是否违背给定的属性。该属性一般用某种时序逻辑（Temporal Logic）公式描述，并以此为基础生成相应的监控器。因此，在运行时验证中，可将监控器更加具体地定义为“读取有穷运行路径并给出相应结论的装置”^[4]。

在运行时验证中，线性时序逻辑（Linear Temporal Logic, LTL）^[14]作为一种广泛用于描述反应式系统属性的形式规约，获得较多关注和研究^[15-16]。为了增强运行时验证的实时性，可以通过LTL进行扩展来描述实时性质。其中，度量时序逻辑（Metric Temporal Logic, MTL）^[17]是一个广受关注的领域，它是在LTL的基础上，通过给时序算子X、U、R等增加时钟实时性质的描述。然而，MTL在密集时间域上的满足性是不可判定的^[18]，因此，研究者通过限制MTL语法来得到可判定性，从而产生了MTL的子集度量区间时序逻辑（Metric Interval Temporal Logic, MITL）^[18]、定量时序逻辑（Quantitative Temporal Logic, QTL）^[19]、信号时序逻辑（Signal Temporal Logic, STL）^[20]等。一些学者对MTL这一些子集的可判定性进行了分析，并对其复杂度进行了比较^[21]。此外，还有采用时间命题时序逻辑（Timed Propositional Temporal Logic, TPTL）^[22]、实时逻辑（Real-Time Logic, RTL）^[23]、动态通信自动机（Dynamic Automata with Timers and Events, DATEs）^[24]等。为了描述某些更为复杂的需求（如多机器人协同性质、安全性质等），研究人员就这一问题提出了超性质（Hyperproperty）的概念，将形式逻辑语义从单条路径扩展到路径集合^[25]。Clarkson等^[26-27]进一步提出HyperLTL的概念，给出超性质在该逻辑下的监控框架。

在监控器构造方面，一般由基于约束图、基于逻辑重写和基于自动机3种方式来构造实时性质的监控器。对于基于约束图的方法，相关研究中有代表性的是使用基于RTL的规约语言来表示时间约束的方法^[28-29]。首先通过构造时间约束的约束图，将约束图作为监控器，然后在运行时根据获取到的事件信息，对约束图进行实例化，通过寻找图中是否存在负环来判断性质是否满足。基于逻辑重写的方法在实时领域中研究得更多一些^[30-31]，如针对实时LTL和MTL的基于逻辑重写的验证方法。该方法以on-the-fly的方式将性质公式重写为正则形式，通常通过逻辑的不动点刻画来实现，运行时只需保存下一状态需满足的公式。近年来，基于自动机理论根据实时时序逻辑构造时间自动机（Timed Automata）^[32⇓-34]，并将时间自动机的扩展形式作为监控器，也是一个重要方向。除上述监控方法外，还有不少相关的研究工作^{[35⇓⇓⇓⇓-40]}，受限于篇幅，在此不再一一阐述。

上述验证方法多基于逻辑的两值语义，有时不能尽早地发现性质背离，而这一点对于监控实时性质来说非常重要。Leucker等^[41⇓-43]对基于TLTL三值语义的运行时验证进行研究，扩展了LTL的标准语义，增加了表示“不确定”的状态“?”，釆用事件时钟自动机作为监控器形式化描述，通过求性质公式及其取反公式的相应事件时钟自动机的笛卡儿积，得到三值语义监控器，监控过程中采用符号化执行的方式来判定系统执行是否满足或违背性质规约。在信息不完善的情况下，三值语义能够更明确地进行表达。此外，Bauer等^[44]提出的RV-LTL为四值语义，其对不确定状态的LTL属性可进一步进行可能为真或者可能为假的推测。

近年来，对人机物融合系统进行运行时验证越来越受到重视。例如，Mitsch等^[45]将定理证明合成监控器的方法用于信息物理融合系统（Cyber-Physical System, CPS）的运行时验证;Fraigniaud等^[46]利用去中心化思想将RV运用于分布式系统的监控;Pedro等^[47]利用MTL语言实现对实时系统的监控;Singh等^[48]将STL用于CPS的软件测试。随着无人系统更加广泛地应用于民生和国防各领域，采用运行时验证技术对无人系统进行监控的相关研究也相继出现。例如，Kane等^[49]利用独立硬件实现对自主驾驶系统的运行时验证，Aiello等^[50]利用运行时保证技术实现对关键飞行控制系统的监控。除了CPS，RV在商业软件方面也有广泛的应用前景，例如Luo等^[51]利用RV进行云服务工作流时序的一致性检测等。

RV关注于已经发生的轨迹分析与监控相似，而近年来在线验证（Online Verification）思想也被提出，并得到广泛关注。其基本思想是在线获取系统运行时参数来构建系统模型，然后基于模型检验方法尽可能高效地验证系统在后续有限时间内的安全性。为实现在线监控，Johnson等^[52]、Chen等^[53]提出了基于集合的线性混成系统在线可达性验证方法。Chen等^[54]还通过对非线性混成系统进行简化，将已有方法扩展到非线性系统的在线监控。

1.2 运行时增强

在监控器生成和部署后，虽然以在线实时的方式能够得到性质的满足与违反判定结果，但在安全攸关系统中这还并不足够。为了在运行过程中自动化地及时发现安全性恶意行为并进行相应控制防护，最早在2000年，由Schneider^[55]提出了将传统运行时验证、控制、增强等手段相结合，自动生成安全代码，以弥补运行时验证理论在动态环境不确定因素方面防护能力的欠缺。

与运行时验证的区别是，除了可以对软件在运行时的非正常行为进行监控，当异常行为发生时，还可以采取一些增强措施来保持某些关键安全性质，即软件运行时增强（Runtime Enforcement, RE）技术。运行时增强方面的研究最早开始在安全自动机上开展，其原理是通过强制监控器监控当前执行序列是否违背期望性质，如果监控到违反，可以通过立即中止程序运行的方式来避免重大的安全问题。

此后，又有了大量的对增强机制的研究，以及对可增强属性的探索，将属性范围拓展到除安全性质以外更广泛的应用中，并提出了更加强大的安全防护代码模型，也出现了运行时增强工具等^[56-57]，可以将安全约束属性转换为安全增强监控代码。程序在执行任何安全相关操作的上下文时，监控器可以通过插入其他动作，如抑制动作（停止、替换、插入等），或允许输入动作序列不受干扰地执行，促使软件按照安全的行为序列运行。

运行时增强过程如图1所示。在这样一个作用过程中，系统允许进行插装，以即时验证待执行操作是否违反安全性质的监控器，并且允许插入或抑制操作来保证系统的输出始终符合性质，其中的输入操作序列由用户或原系统执行产生，输出序列被发送到安全防护的监控器（也称为强制防护器或防护器）。如图1所示的一个运行时增强过程是一个在系统运行时对Π属性进行防护的决策过程。它读取一个有限（可能是无限）的事件序列σ，然后输出一个新的有限（可能是无限）的事件序列o。安全防护的监控器配备了一个内部存储区和一组对输入事件的操作（时序性质相关的数据可能需要存储）。

增强过程是作用于σ与o之间的一道防护。为了保证防护方法的合理有效，σ与o之间可能还存在一些约束（如透明性）等，从而影响读取输入事件序列σ时防护监控器所采取的强制操作。因此，在构造运行时增强监控器时需要遵守透明性（Transparency）和可靠性（Soundness）^[58]的原则。其中，透明性是指运行时强制方法构造的安全性质防护器在全过程中不应妨碍原系统中正确的执行序列;可靠性是指被防护系统中的不正确执行序列必须被阻止或纠正。除了以上两则约束以外，研究者还总结了一些强制方法中应该尽量考虑的特性（表1），使得强制方法更加优化。

近年来，软件运行时增强技术的研究取得了长足发展。Lanotte等^[59]针对工业控制系统所面临的安全问题，提出了基于运行时增强的形式化方法来增强网络控制器的安全性。Pinisetty等^[60]面向CPS的可靠性问题，提出了心脏起搏系统的闭环运行时增强框架。Hu等^[61]提出的面向机器人系统的运行增强框架，增强了机器人集群在不确定环境下运行时的安全性。

1.3 环境建模、理解与自适应规划

前文从运行时验证、监控和增强的角度对相关工作的整体思路进行了介绍。下文将以工作于开放不确定场景下的实时系统（如自动驾驶、列车控制等）为代表，对软件系统面向外在环境、内在行为的不确定性所开展的建模、验证，特别是动态调控方面的工作进一步展开讨论。

开放不确定场景下软件运行空间充斥着诸多“不确定性”，而这个“不确定性”是贯穿感知—预测—规控上下游的，主要体现在感知局限性，例如车载硬件的感知能力是有局限的，激光探测及测距系统（Light Detection and Ranging, LiDAR）的可靠感知范围不过百米，货车等大型交通参与者也会造成视角遮挡等。忽略这些不确定性的影响进行规划，将导致规划的轨迹不再具有安全的属性，使系统产生不安全行为。为保障行为安全，构建不确定性环境的概率模型，并在此基础上自适应规划概率安全的轨迹是当前的一个主要方向。

规划概率安全轨迹的前提是准确构建环境概率模型。环境中往往存在多种运动模态、形状各异的物体。为了能够准确估计物体的位置和形状信息，需要充分地利用有限的历史观测数据，通过一种基于概率分析的环境构建方法对机器人当前的未知外部环境进行统计分析。在此基础上，轨迹规划方法传播系统的位姿不确定性与环境的概率模型进行交互计算，以映射不确定性到规划的轨迹。在以上规划过程中，环境建模的精度和规划算法的效率问题是两个重要的问题。粗糙的建模过程将导致规划的轨迹过于保守，低效的规划过程不利于实现实时计算而失去规划的实际意义。面向实际的机器人系统规划需求，实现高精度的环境建模和实时的规划是两个必须深入考虑的问题。

实现高精度的环境建模需要从环境中物体的形状和位置两个对规划非常重要的属性分别进行建模。一方面，利用传感器感知的物体形状是随着时间维度不断完善的过程，因此需构建动态的建模方法，通过数据的不断补充实现物体形状的精确建模;另一方面，动态的物体位置预测需考虑多方面的影响，包括物体的运动倾向、运动模型、环境约束等。多种约束的存在应使建模的方法具有较好的拓展框架，可兼容多种约束的影响。在环境建模的基础上，高效的位姿不确定性传播以及与环境模型的交互计算方法是提高规划算法效率的关键。此外，规划过程需要考虑轨迹的质量问题。基于此，规划算法的研究应首先着眼于交互计算方法的优化，然后在规划框架方面体现优化的过程。

当前处理不确定性的方法主要有概率统计理论、模糊理论、粗糙集理论和灰色系统理论等，其中概率方法主要研究随机不确定性信息的描述与表达，理论最为完善，方法最为成熟，是当前移动机器人研究的主流方法^[62]。Barth等^[63]的卡尔曼滤波和蒙特卡罗方法在短距离不确定性的预测场景下可获得较好预测性能。Houenou等^[64]对角速度和加速度进行预测，提高了长时预测的性能。刘志强等^[65]采用传统机器学习方法对运动轨迹进行预测，如隐马尔可夫模型和支持向量机等。李建平等^[66]结合了隐马尔可夫模型和高斯混合模型对车辆历史轨迹进行建模，在较为简单的驾驶环境中取得了较高的预测精度。

不确定条件下的规划过程可被构建为一个部分可观测马尔可夫决策过程（Partially Observable Markov Decision Process, POMDP），机器人从一个不可被完全观测的状态向下一个状态演化，规划的目的是求解控制策略以实现从状态的概率分布到机器人行为的映射过程。基于这个过程，一系列基于求解POMDP的方法被提出以实现多种应用。例如，不确定环境下的无人驾驶^[67]、移动机器人^[68]等。尽管基于POMDP的方法已经在理论和实际实验中显示出了较好的成绩，但求解POMDP的计算效率问题仍旧难以解决，尤其是考虑高动态的环境下，无法实时计算的算法难以跟上环境的变化。

为了简化计算难度，另外一种处理不确定性的方法将该类问题转化为求解机会约束优化问题。Blackmore等^[69]针对威胁的不确定性，提出了基于机会约束的路径规划方法，虽然这种优化已被证明可用于实时路径规划，但它在复杂和动态环境中可扩展性较差。Zhu等^[70]将机会约束和模型预测控制结合在一起，在滚动优化的框架下实现机会约束的求解以确保在存在感知和定位不确定性的条件下多个无人机之间无碰撞。Arantes等^[71]针对如何平衡不确定性条件下的规划问题和安全问题展开了研究，通过确保机器人在连续2个时间步之间的安全性满足机会不等式约束。这些利用机会约束优化的方法从多个维度对机会约束优化的算法展开了研究，然而这些算法大多只在仿真环境下应用，对于如何平衡实际机器人需求的效率、安全、优化等问题仍没有很好的解决方案。

1.4 实时行为建模、验证与动态调控

开放不确定场景下软件行为中离散跳转与连续行为紧密交织，这样的特性决定了混成自动机（Hybrid Automata, HA）^[72]是其最自然的建模语言之一。目前，对混成自动机的建模与验证研究主要集中在混成自动机的安全性（Safety）检验上，其直观概念可以解读为系统运行中是否会发生不好的行为。安全性检验，即检验从给定的初始条件出发，系统运行中是否会出现违背规约或者不安全的行为。由于混成自动机的运行既包含状态的离散变化，又包含状态的连续变化，其相应的模型检验问题十分困难。目前对混成自动机的模型检验主要集中在安全性的一个子集——可达性（Reachability）问题上。

与可达性验证有所不同，混成系统的控制问题旨在找到一组系统外部的控制输入和系统的控制模式序列，使得对应的系统行为能满足系统内部和外部环境的所有安全性约束以及特定的控制目标。要完成混成系统的最优控制生成，就是要找到尽可能最优的外部控制输入和控制模式序列^[73]。

对于可微混成系统，主流的控制生成方法是基于梯度下降的。Xu等^[74]首先提出了经典的基于梯度的双层优化算法，在顶层生成控制序列，在底层基于梯度优化求解最优外部输入。在此基础上，Egerstedt等^[75]基于最速下降法来加速底层外部输入的优化求解过程，CaldWell等^[76]、Johnson等^[77]则是使用基于梯度下降法来加速底层优化求解。除此之外，Gonzalez等^[78]、Ali等^[79]也设计了各种算法来加速顶层控制模式序列的优化求解过程。除了主流的基于梯度的可微混成系统控制生成方法，Nilsson等^[80]和Ding等^[81]也提出了一些基于数值计算的控制生成方法。

对于不可微混成系统，由于梯度信息难以获取，主流的控制生成方法是基于采样和各种启发式搜索来进行控制生成。例如，Branicky等^[82]基于路径规划中的快速扩展随机生成树（Rapidly-exploring Random Trees, RRTs）算法进行控制生成，但缺少最优性的理论保障。此后，Farahani等^[83]提出了一种鲁棒的稳定模型预测控制生成（Model Predictive Control, MPC）方法，基于蒙特卡罗模拟拒绝采样（Monte Carlo Simulation and Rejection Sampling, MCRS）来解决最坏情况下的MPC控制问题，不过其处理复杂控制任务的能力相对有限。如何对给定的混成系统快速高效地生成控制参数仍是一个亟待解决的问题。

上述验证与控制方法通过在系统运行前形式化地验证系统安全性，来保障系统运行时的安全。然而，对于实际问题中规模极大、复杂性极高、系统环境参数在运行时才能确定的软件系统，上述验证与控制方法难以在系统运行前完成对其安全性的验证。因此，Sha等^[84]提出了Simplex的架构思想，即通过系统在线监控使得系统在高性能但不保证安全的控制策略与低性能但已被验证安全的控制策略间切换。例如，一旦在线监控预测到了系统某一安全性质即将被违背时，则将系统控制策略切换成安全的备用策略。系统在线监控能否及时有效地预测到系统的不安全行为是该Simplex架构的关键。近年来，基于在线验证对于系统实时行为进行快速在线建模，并对状态安全性进行验证也是相关领域的一个重点关注方向。Pek等^[85]通过在线验证对自动驾驶的运行时安全进行验证并进行干预来保证系统运行安全。

2 国内研究进展

收起

在上述运行时验证、监控、增强、动态调控等领域，国内学者也进行了长期的研究与探索，并取得了系列进展与成果，选取其中部分工作介绍如下。

（1）在基于运行时验证的软件监控方面，国防科技大学团队围绕如何在系统错误发生之前进行预测并开展长期研究。他们提出在系统运行前即提取出被监控系统的模型以及根据属性规约来自动产生运行时监控器，运行时阶段，将当期系统执行路径所需要的前瞻信息从模型中收集，以判定未来执行路径是否将违背被监控的属性和规约^[86]，在此基础上进一步提出了基于程序代码的静态分析方法来辅助运行时监控的预测。此外，他们提出在运行时对代码段进行分析，从而得到辅助信息来进行预测^[87]，对于复杂系统来说，这无疑更有可取性。

南京航空航天大学团队研究了内存安全性和形式化规约的运行时监控技术：在内存安全性方面，提出了基于智能状态的监控算法^[88]和源代码级别的插桩框架^[89-90]，并实现了工具Movec^[91];在形式化规约方面，提出了C程序参数化运行时验证算法^[92]，证明了参数化运行时验证的时间复杂度是NP完全的^[93]，提出了规约的四值可监控性概念及其判定算法^[94]。

（2）在基于运行时验证的软件调控方面，南京大学在混成系统在线验证与控制方面进行了长期探索。针对CPS在开放不确定场景下的动态行为监控问题，南京大学团队提出了面向带参混成自动机的安全攸关场景驱动在线验证方式。通过对系统后续短期状态空间进行在线快速前瞻式验证，发现风险并提前进行预警^[95]。此外，相关团队研究了基于无梯度优化的混成系统控制生成方式，使得对复杂混成系统在线生成控制参数成为可能^[96-97]。在此基础上，进一步提出了将在线验证与控制生成相结合的运行时安全保障方法，当在线验证发现后续潜在风险时，在线生成安全控制参数，接管系统行为，从而形成一个可以对动态系统后续状态空间在线验证，并对潜在危险进行预测、反馈与干预的新型在线容错方法，保障系统运行安全^[98]。相关工作已经在轨道交通、智能制造、智能驾驶等领域展开实例研究。

中国科学院软件研究所（简称软件所）团队在（随机）混成系统安全性验证方面取得突破，尤其在可达-规避分析方面做了大量理论研究，例如构建了刻画可达-规避集合表达能力强的凸约束^[99⇓-101]。基于这方面的研究，以及当前智能驾驶等安全攸关系统的需要，软件所团队也开展了基于可达-规避分析的安全控制律生成的研究，通过提出高效的（鲁棒）约束求解算法来有效地生成安全控制率，服务于安全攸关系统（如智能驾驶）的实时控制。

（3）针对CPS中的扰动信号及不确定环境，华东师范大学基于STL，增加刻画扰动信号的算子，提出能够刻画扰动范围的扰动信号时态逻辑（Perturbed Signal Temporal Logic, PertSTL），并提出一种面向PertSTL的在线检测方法，从而帮助分析一定范围内的信号扰动对验证结果产生的最坏影响。该方法已成功应用于汽车自动驾驶场景、智能建筑的温控系统的在线检测，能有效分析信号扰动对系统安全性的影响。

（4）在系统级层面，中山大学无人系统团队在混合关键级系统方面做了许多理论研究工作，特别是在面向最坏情况执行时间（Worst-Case Execution Time, WCET）的运行时监控和自适应调整方面，包括形式化验证^[102-103]、在线监控^[104-105]、自适应调整^[106]等方面，提出了包括自适应能量管理、自适应工作流管理等先进方法和理论，服务于无人系统的实时在线运行。此外，团队在应用于实时系统的规划和控制方面进行了较为深入的研究工作，并应用到了无人驾驶车辆规划^[107]、转向控制^[108]、水面自主航行可通行区域建模^[109]、海面目标跟踪^[110]等领域，取得了显著的效果。

通过对近年来国内学者在基于形式化建模与验证等手段的复杂软件在线监控等领域的部分代表性工作进行总结（事实上在更广泛的自动控制领域还有着大量工作，囿于本文主题所限，未在文章中进行整体总结），可以看出国内学者在软件运行时验证、监控、动态调控等方向的理论、算法、工具等方面均取得了一系列显著的进展，并且已经在轨道交通、智能制造、无人车、无人船等领域进行应用验证。如何进一步推动相关研究，特别是面向智能时代下复杂软件所面临的挑战，形成开放不确定场景下软件运行时验证、监控、与动态调控的方法与体系，有待相关领域产学研深入协作与研究。

3 发展趋势与建议

收起

通过对运行时验证、监控、增强及动态调控等方面的国内外研究进展的介绍与总结可以看出，相关领域得到了国内外专家学者的广泛关注与持续研究，并取得了系列重要成果。然而，随着“开放不确定”这一关键词成为轨道交通、航空航天、智能驾驶、智能制造等国家重要战略发展领域软件运行的新常态，并且伴随着智能化浪潮带来的巨大变革，相关领域仍有大量工作亟待解决。关于中国在该领域的后续研究，提出以下几点建议。

（1）面向开放不确定环境的概率建模与轨迹规划。概率化建模软件运行环境中物体的位置、分布等信息，使软件对所处环境进行充分理解，并进行在线快速路径规划与调整，以保证系统运行安全，是面向开放不确定场景挑战的重要方向之一。

（2）面向实时动态行为的软件行为建模与控制生成。在静态建模语言方面进行拓展，分别在动态参数、动态交互拓扑等层面进行参数化描述与运行时模型实例化，准确刻画系统实际行为，以帮助后续运行时监控与验证实时、准确捕获当前系统行为，是有效在线监控的必由之路。

（3）面向安全容错的软件行为控制器自学习。由于系统行为中各种动态行为高发，传统的基于正向推导的离线静态设计方法难以对相关复杂系统生成安全控制逻辑。基于智能化学习技术构建安全可信的系统控制器，是相关领域近年来的重点关注所在。

（4）面向黑盒不可解释系统的运行时监控与调控。当前各类信息物理系统中包含越来越多的智能组件，如神经网络模型等，其结构复杂、参数众多，难以对其具体行为和决策进行解释，为了确保这些组件运行结果的安全性和可靠性，对其行为进行运行时监控和调控非常必要。

（5）覆盖软件运行全生命周期的运行时监控与反馈。从软件系统架构角度研究一种新的系统设计方案，将基于在线验证与控制的系统容错机制纳入系统设计，使得运行系统与监控模块间可以无缝交互，保障系统运行，具有重要意义。

4 结束语

收起

在开放不确定场景下，软件与外界密切交互，主动感知并构建外界环境与自身行为模型，实时形成控制策略并快速执行，以期提供及时、精确且安全可靠的服务。面向相关高度动态、不确定行为，对其进行准确的形式化建模、验证与监控，并进行动态调控是保障相关软件准确、高效运行的重要手段。在此基础上进一步研究并形成完整的复杂软件系统运行时可信保障技术与方案，开发有效的运行时验证、监控、调控等工具，并服务于轨道交通、航空航天、智能驾驶、智能制造等国家重要发展领域，具有重要研究意义与应用前景。

基金

收起

国家自然科学基金(62232008)
国家自然科学基金(62172200)
国家自然科学基金(62032019)
江苏省前沿引领技术基础研究专项(BK20202001)
广东省粤穗联合基金青年基金(2020A1515110199)
深圳市基础研究项目(JCYJ20210324122203009)
深圳市基础研究项目(JCYJ20180508152434975)

参考文献

收起

文献

收起

参考文献引证文献

排序方式：

[1]

Bertot

, Castéran

. Interactive theorem proving and program development[M]. Berlin, Heidelberg: Springer, 2004.

[2]

Clarke

E M

, Grumberg

, Peled

. Model checking[C]// Ramesh S, Sivakumar G. Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1997. Berlin, Heidelberg: Springer, 1997: 54-56.

[3]

Myers

. The art of software testing[M]. Hoboken: John Wiley & Sons, Inc., 2004.

[4]

Leucker

, Schallhart

. A brief account of runtime verification[J]. The Journal of Logic and Algebraic Programming, 2009, 78(5): 293-303.

https://doi.org/10.1016/j.jlap.2008.08.004

[5]

Snodgrass

. A relational approach to monitoring complex systems[J]. ACM Transactions on Computer Systems, 1988, 6(2): 157-195.

https://doi.org/10.1145/42186.42323

[6]

IEEE.IEEE Standard Glossary of Software Engineering Terminology:IEEE Std 610.12-1990[S]. Piscataway: IEEE Press, 1990.

[7]

Zulkernine

, Seviora

R E

. A compositional approach to monitoring distributed systems[C]// Proceedings of the International Conference on Dependable Systems and Networks. Piscataway: IEEE Press, 2001: 763-772.

[8]

Bauer

, Leucker

, Schallhart

. Model-based runtime analysis of distributed reactive systems[C]// Proceedings of the Australian Software Engineering Conference (ASWEC’06). Piscataway:IEEE Press, 2006: 243-252.

[9]

Gopinathan

, Rajamani

S K

. Runtime monitoring of object invariants with guarantee[C]// Leucker M.Proceedings of the International Workshop on Runtime Verification. Berlin, Heidelberg: Springer, 2008: 158-172.

[10]

G Z

, Hariri

, Jangiti

, et al. Online monitoring and analysis for self-protection against network attacks[C]// Proceedings of the International Conference on Autonomic Computing, 2004. Piscataway: IEEE Press, 2004: 324-325.

[11]

Reinbacher

, Rozier

K Y

, Schumann

. Temporal-logic based runtime observer Pairs for system health management of real-time systems[C]// Ábrahám E, Havelund K. Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014. Berlin, Heidelberg: Springer, 2014: 357-372.

[12]

Lattanzi

, Acquaviva

, Bogliolo

. Run-time software monitor of the power consumption of wireless network interface cards[C]// Macii E, Paliouras V, Koufopavlou O. Proceedings of the International Workshop on Power and Timing Modeling, Optimization and Simulation. Berlin, Heidelberg: Springer, 2004: 352-361.

[13]

L G

. Applying software wrapping on performance monitoring of web services[J]. Journal of Computer Science, 2007, 6(3): 1-6.

https://doi.org/10.3844/jcssp.2010.1.11

[14]

Pnueli

. The temporal logic of programs[C]// Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS 1977). Piscataway:IEEE Press, 2008: 46-57.

[15]

Geilen

. On the construction of monitors for temporal logic properties[J]. Electronic Notes in Theoretical Computer Science, 2001, 55(2):181-199.

https://doi.org/10.1016/S1571-0661(04)00252-X

[16]

Havelund

, Roşu

. Synthesizing monitors for safety properties[C]// Katoen J P, Stevens P.Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 2002: 342-356.

[17]

Alur

, Feder

, Henzinger

T A

. The benefits of relaxing punctuality[J]. Journal of the ACM, 1996, 43(1): 116-146.

https://doi.org/10.1145/227595.227602

[18]

Ouaknine

, Worrell

. On the decidability of metric temporal logic[C]// Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05). Piscataway:IEEE Press, 2005: 188-197.

[19]

Hirshfeld

, Rabinovich

. Logics for real time: Decidability and complexity[J]. Fundamenta Informaticae, 2004, 62(1): 1-28.

[20]

Maler

, Nickovic

. Monitoring temporal properties of continuous signals[C]// Lakhnech Y, Yovine S.Proceedings of the International Conference on Formal Techniques, Modelling and Analysis of Timed and Fault-tolerant Systems. Berlin, Heidelberg: Springer, 2004: 152-166.

[21]

Konur

. A survey on temporal logics for specifying and verifying real-time systems[J]. Frontiers of Computer Science, 2013, 7(3): 370-403.

https://doi.org/10.1007/s11704-013-2195-2

[22]

Alur

, Henzinger

T A

. A really temporal logic[J]. Journal of the ACM, 1994, 41(1): 181-203.

https://doi.org/10.1145/174644.174651

[23]

Ostroff

J S

. Temporal logic for real-time systems[M]. Taunton: Research Studies Press, 1989.

[24]

Colombo

, Pace

G J

, Schneider

. Dynamic event-based runtime monitoring of real-time and contextual properties[C]// Cofer D, Fantechi A. Proceedings of the International Workshop on Formal Methods for Industrial Critical Systems. Berlin, Heidelberg: Springer, 2009: 135-149.

[25]

Clarkson

M R

, Schneider

F B

. Hyperproperties[C]// Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium. Piscataway: IEEE Press, 2008: 51-65.

[26]

Clarkson

M R

, Finkbeiner

, Koleini

, et al. Temporal logics for hyperproperties[DB/OL]. arXiv preprint: 1401.4492, 2014.

[27]

Agrawal

, Bonakdarpour

. Runtime verification of k-safety hyperproperties in HyperLTL[C]// Proceedings of the 2016 IEEE 29th Computer Security Foundations Symposium (CSF). Piscataway:IEEE Press, 2016: 239-252.

[28]

Mok

A K

, Liu

G T

. Efficient Run-time monitoring of timing constraints[C]// Proceedings of the Third IEEE Real-time Technology and Applications Symposium. Piscataway: IEEE Press, 2002: 252-262.

[29]

Jahanian

, Rajkumar

, Raju

S C V

. Runtime monitoring of timing constraints in distributed real-time systems[J]. Real-time Systems, 1994, 7(3): 247-273.

https://doi.org/10.1007/BF01088521

[30]

Kristoffersen

K J

, Pedersen

, Andersen

H R

. Runtime verification of timed LTL using disjunctive normalized equation systems[J]. Electronic Notes in Theoretical Computer Science, 2003, 89(2): 210-225.

https://doi.org/10.1016/S1571-0661(04)81050-8

[31]

Thati

, Roşu

. Monitoring algorithms for metric temporal logic specifications[J]. Electronic Notes in Theoretical Computer Science (ENTCS), 2005, 113(C): 145-162.

[32]

Kini

D R

, Krishna

S N

, Pandya

P K

. On construction of safety signal automata for MITL[u, s] using temporal projections[C]// Fahrenberg U, Tripakis S. Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems. Berlin, Heidelberg: Springer, 2011: 225-239.

[33]

Geilen

, Dams

. An on-the-fly tableau construction for a real-time temporal logic[C]// Joseph M.Proceedings of the 6th International Symposium on Formal Techniques in Real-time and Fault-tolerant Systems.Berlin, Heidelberg: Springer, 2000: 276-290.

[34]

Drusinsky

. On-line monitoring of metric temporal logic with time-series constraints using alternating finite automata[J]. Journal of Universal Computer Science, 2006, 12(5): 482-498.

[35]

Basin

, Klaedtke

, Müller

, et al. Monitoring metric first-order temporal properties[J]. Journal of the ACM, 2015, 62(2): 1-45.

[36]

Basin

, Klaedtke

, Zălinescu

. Algorithms for monitoring real-time properties[J]. Acta Informatica, 2018, 55(4): 309-338.

https://doi.org/10.1007/s00236-017-0295-4

[37]

Simko

, Sztipanovits

. Active monitoring using real-time metric linear temporal logic specifications[C]// Conchon E, Correia

C M B A

, Fred

A L N

, et al.Proceedings of the International Conference on Health Informatics. 2012, doi: 10.5220/0003768703700373.

[38]

Pinisetty

, Falcone

, Jéron

, et al. Runtime enforcement of timed properties[C]// Qadeer S, Tasiran S.Proceedings of the 4th International Conference on Runtime Verification. Berlin, Heidelberg: Springer, 2013: 229-244.

[39]

Baldor

, Niu

J W

. Monitoring dense-time, continuous-semantics, metric temporal logic[C]// Qadeer S, Tasiran S. Proceedings of the 4th International Conference on Runtime Verification. Berlin, Heidelberg: Springer, 2013: 245-259.

[40]

de Matos Pedro

, Pereira

, Pinho

L M

, et al. A compositional monitoring framework for hard real-time systems[C]// Badger J M, Rozier K Y. Proceedings of the 6th NASA Formal Methods Symposium. Cham: Springer, 2014: 16-30.

[41]

Bauer

, Leucker

, Schallhart

. Monitoring of real-time properties[C]// Arum-Kumar S, Grag N.Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science. Berlin, Heidelberg: Springer, 2006: 260-272.

[42]

Arafat

, Bauer

, Leucker

, et al. Runtime verification revisited[R]. Munich: Technical University of Munich, 2005.

[43]

Bauer

, Leucker

, Schallhart

. Runtime verification for LTL and TLTL[J]. ACM Transactions on Software Engineering and Methodology, 2011, 20(4), doi: 10.1145/2000799.2000800.

https://doi.org/10.1145/2000799.2000800

[44]

Bauer

, Leucker

, Schallhart

. The good, the bad, and the ugly, but how ugly is ugly?[C]// Sokolsky O, Taşiran S. Proceedings of the 7th International Workshop on Runtime Verification. Berlin, Heidelberg: Springer, 2007: 126-138.

[45]

Mitsch

, Platzer

. ModelPlex: Verified runtime validation of verified cyber-physical system models[J]. Formal Methods in System Design, 2016, 49(1-2): 33-74.

https://doi.org/10.1007/s10703-016-0241-z

[46]

Fraigniaud

, Rajsbaum

, Travers

. On the number of opinions needed for fault-tolerant run-time monitoring in distributed systems[C]// Bonakdarpour B, Smolka S A. Proceedings of the 5th International Conference on Runtime Verification. Cham: Springer, 2014: 92-107.

[47]

de Matos Pedro

, Pereira

, Pinho

L M

, et al. Monitoring for a decidable fragment of MTL-∫[M]// Bartocci

, Majumdar

. Runtime

Verification

. Cham: Springer International Publishing, 2015: 169-184.

[48]

Singh

N K

, Saha

. Specification-guided automated debugging of CPS models[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, 39(11): 4142-4153.

https://doi.org/10.1109/TCAD.43

[49]

Kane

, Chowdhury

, Datta

, et al. A case study on runtime monitoring of an autonomous research vehicle (ARV) system[M]// Bartocci

, Majumdar

. Proceedings of the 6th Runtime Verification. Cham: Springer, 2015: 102-117.

[50]

Aiello

, Berryman

, Grohs

, et al. Run-time assurance for advanced flight-critical control systems*[C]// AIAA Guidance, Navigation, and Control Conference. Reston: AIAA, 2010, doi: 10.2514/6.2010-8041.

[51]

Luo

H Y

, Liu

, et al. Runtime verification of business cloud workflow temporal conformance[J]. IEEE Transactions on Services Computing, 2022, 15(2): 833-846.

https://doi.org/10.1109/TSC.2019.2962666

[52]

Johnson

T T

, Bak

, Caccamo

, et al. Real-time reachability for verified simplex design[J]. ACM Transactions on Embedded Computing Systems, 2016, 15(2): 1-27.

[53]

Chen

, Sankaranarayanan

. Model predictive real-time monitoring of linear systems[C]// Proceedings of the 2017 IEEE Real-time Systems Symposium (RTSS). Piscataway:IEEE Press, 2018: 297-306.

[54]

Chen

, Sankaranarayanan

. Decomposed reachability analysis for nonlinear systems[C]// Proceedings of the 2016 IEEE Real-time Systems Symposium (RTSS). Piscataway:IEEE Press, 2017: 13-24.

[55]

Schneider

F B

. Enforceable security policies[C]// Foundations of Intrusion Tolerant Systems, 2003. Piscataway: IEEE Press, 2004: 117-137.

[56]

Falcone

. You should better enforce than verify[C]// Barringer H, Falcone Y, Finkbeiner B, et al.Proceedings of the First International Conference on Runtime Verification. Berlin, Heidelberg: Springer, 2010: 89-105.

[57]

Ligatti

, Bauer

, Walker

. Run-time enforcement of nonsafety policies[J]. ACM Transactions on Information and System Security, 2009, 12(3): 1-41.

[58]

Lanotte

, Merro

, Munteanu

. Runtime enforcement for control system security[C]// Proceedings of the 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). Piscataway:IEEE Press, 2020: 246-261.

[59]

Lanotte

, Merro

, Munteanu

. Industrial control systems security via runtime enforcement[J]. ACM Transactions on Privacy and Security, 2023, 26(1): 1-41.

[60]

Pinisetty

, Roop

P S

, Smyth

, et al. Runtime enforcement of cyber-physical systems[J]. ACM Transactions on Embedded Computing Systems, 2017, 16(5s): 1-25.

[61]

, Dong

, Yang

, et al. Decentralized runtime enforcement for robotic swarms[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(11): 1591-1606.

[62]

Blanco

J L

, Fernandez-Madrigal

J A

, Gonzalez

. Efficient probabilistic range-only SLAM[C]// Proceedings of the 2008 IEEE/RSJ International Conference on Intelligent Robots and Systems. Piscataway: IEEE Press, 2008: 1017-1022.

[63]

Barth

, Franke

. Where will the oncoming vehicle be the next second?[C]// Proceedings of the 2008 IEEE Intelligent Vehicles Symposium. Piscataway: IEEE Press, 2008: 1068-1073.

[64]

Houenou

, Bonnifait

, Cherfaoui

, et al. Vehicle trajectory prediction based on motion model and maneuver recognition[C]// Proceedings of the 2013 IEEE/RSJ International Conference on Intelligent Robots and Systems. Piscataway: IEEE Press, 2014: 4363-4369.

[65]

刘志强, 吴雪刚, 倪捷, 等. 基于HMM和SVM级联算法的驾驶意图识别[J]. 汽车工程, 2018, 40(7): 858-864.

[66]

李建平. 面向智能驾驶的交通车辆运动预测方法研究[D]. 长春: 吉林大学, 2018.

[67]

Hubmann

, Quetschlich

, Schulz

, et al. A POMDP maneuver planner for occlusions in urban scenarios[C]// Proceedings of the 2019 IEEE Intelligent Vehicles Symposium (IV). Piscataway:IEEE Press, 2019: 2172-2179.

[68]

Sun

, Schlotfeldt

, Pappas

G J

, et al. Stochastic motion planning under partial observability for mobile robots with continuous range measurements[J]. IEEE Transactions on Robotics, 2021, 37(3): 979-995.

https://doi.org/10.1109/TRO.2020.3042129

[69]

Blackmore

, Ono

, Williams

B C

. Chance-constrained optimal path planning with obstacles[J]. IEEE Transactions on Robotics, 2011, 27(6): 1080-1094.

https://doi.org/10.1109/TRO.2011.2161160

[70]

Zhu

, Alonso-Mora

. Chance-constrained collision avoidance for MAVs in dynamic environments[J]. IEEE Robotics and Automation Letters, 2019, 4(2): 776-783.

https://doi.org/10.1109/LRA.2019.2893494

[71]

da Silva Arantes M, Toledo

C F M

, Williams

B C

, et al. Collision-free encoding for chance-constrained nonconvex path planning[J]. IEEE Transactions on Robotics, 2019, 35(2): 433-448.

https://doi.org/10.1109/TRO.8860

[72]

Henzinger

T A

. The theory of hybrid automata[C]// Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science. Piscataway: IEEE Press, 2002: 278-292.

[73]

Branicky

M S

, Borkar

V S

, Mitter

S K

. A unified framework for hybrid control: Model and optimal control theory[J]. IEEE Transactions on Automatic Control, 1998, 43(1): 31-45.

https://doi.org/10.1109/9.654885

[74]

X P

, Antsaklis

P J

. Results and perspectives on computational methods for optimal control of switched systems[C]// Maler O, Pnueli A.Proceedings of the 6th International Workshop on Hybrid Systems:Computation and Control. Berlin, Heidelberg: Springer, 2003: 540-555.

[75]

Egerstedt

, Wardi

, Axelsson

. Transition-time optimization for switched-mode dynamical systems[J]. IEEE Transactions on Automatic Control, 2006, 51(1): 110-115.

https://doi.org/10.1109/TAC.2005.861711

[76]

Caldwell

T M

, Murphey

T D

. An adjoint method for second-order switching time optimization[C]// Proceedings of the 49th IEEE Conference on Decision and Control (CDC). Piscataway:IEEE Press, 2011: 2155-2162.

[77]

Johnson

E R

, Murphey

T D

. Second-order switching time optimization for nonlinear time-varying dynamic systems[J]. IEEE Transactions on Automatic Control, 2011, 56(8): 1953-1957.

https://doi.org/10.1109/TAC.2011.2150310

[78]

Gonzalez

, Vasudevan

, Kamgarpour

, et al. A descent algorithm for the optimal control of constrained nonlinear switched dynamical systems[C]// Proceedings of the 13th ACM international conference on Hybrid systems:Computation and control. New York: ACM Press, 2010: 51-60.

[79]

Ali

, Egerstedt

. Hybrid optimal control under mode switching constraints with applications to pesticide scheduling[J]. ACM Transactions on Cyber-Physical Systems, 2018, 2(1): 1-17.

[80]

Nilsson

, Ozay

. Incremental synthesis of switching protocols via abstraction refinement[C]// Proceedings of the 53rd IEEE Conference on Decision and Control. Piscataway: IEEE Press, 2015: 6246-6253.

[81]

Ding

X C

, Wardi

, Egerstedt

. On-line optimization of switched-mode dynamical systems[J]. IEEE Transactions on Automatic Control, 2009, 54(9): 2266-2271.

https://doi.org/10.1109/TAC.2009.2026864

[82]

Branicky

M S

, Curtiss

M M

, Levine

J A

, et al. RRTs for nonlinear, discrete, and hybrid planning and control[C]// Proceedings of the 42nd IEEE International Conference on Decision and Control (IEEE Cat. No.03CH37475). Piscataway:IEEE Press, 2004: 657-663.

[83]

Farahani

S S

, Raman

, Murray

R M

. Robust model predictive control for signal temporal logic synthesis[J]. IFAC-PapersOnLine, 2015, 48(27): 323-328.

https://doi.org/10.1016/j.ifacol.2015.11.195

[84]

Sha

. Using simplicity to control complexity[J]. IEEE Software, 2001, 18(4): 20-28.

[85]

Pek

, Manzinger

, Koschi

, et al. Using online verification to prevent autonomous vehicles from causing accidents[J]. Nature Machine Intelligence, 2020, 2(9): 518-528.

https://doi.org/10.1038/s42256-020-0225-y

[86]

Zhao

C Z

, Dong

, Qi

Z C

. Active monitoring for control systems under anticipatory semantics[C]// Proceedings of the 2010 10th International Conference on Quality Software. Piscataway: IEEE Press, 2010: 318-325.

[87]

, Chen

Z B

, Dong

. A predictive runtime verification framework for cyber-physical systems[C]// Proceedings of the 2014 IEEE Eighth International Conference on Software Security and Reliability-Companion. Piscataway: IEEE Press, 2014: 223-227.

[88]

Chen

, Wang

, Yan

J Q

, et al. Runtime detection of memory errors with smart status[C]// Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York: ACM Press, 2021: 296-308.

[89]

Chen

, Yan

J Q

, Kan

S L

, et al. Detecting memory errors at runtime with source-level instrumentation[C]// Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York: ACM Press, 2019: 341-351.

[90]

Chen

, Zhang

, Wu

, et al. A source-level instrumentation framework for the dynamic analysis of memory safety[J]. IEEE Transactions on Software Engineering, 2022, doi: 10.1109/TSE.2022.3210580.

https://doi.org/10.1109/TSE.2022.3210580

[91]

Chen

, Wu

, Zhang

, et al. A dynamic analysis tool for memory safety based on smart status and source-level instrumentation[C]// Proceedings of the 2022 IEEE/ACM 44th International Conference on Software Engineering:Companion Proceedings (ICSE-Companion). Piscataway:IEEE Press, 2022: 6-10.

[92]

Chen

, Wang

Z M

, Zhu

Y L

, et al. Parametric runtime verification of C programs[C]// Chechik M, Raskin J F. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 2016: 299-315.

[93]

Chen

. Parametric runtime verification is NP-complete and coNP-complete[J]. Information Processing Letters, 2017, 123: 14-20.

https://doi.org/10.1016/j.ipl.2017.02.006

[94]

Chen

, Chen

Y Y

, Hierons

R M

, et al. Four-valued monitorability of ω-regular languages[C]// Lin S W, Hou Z, Mahony B. Proceedings of the 22nd International Conference on Formal Methods and Software Engineering. Cham: Springer, 2020: 198-214.

[95]

, Wang

Q X

, Ren

X Y

, et al. Scenario-based online reachability validation for CPS fault prediction[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, 39(10): 2081-2094.

https://doi.org/10.1109/TCAD.43

[96]

Wang

J W

, Bu

, Xing

S P

, et al. PDF: Path-oriented, derivative-free approach for safety falsification of nonlinear and nondeterministic CPS[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022, 41(2): 238-251

https://doi.org/10.1109/TCAD.2021.3056360

[97]

Xing

S P

, Wang

J W

, Bu

, et al. Approximate optimal hybrid control synthesis by classification-based derivative-free optimization[C]// Proceedings of the 24th International Conference on Hybrid Systems:Computation and Control. New York: ACM Press, 2021: 10.1145/3447928.3456658.

[98]

Wang

J W

, Bu

, Xing

S P

, et al. Combined online checking and control synthesis: A study on a vehicle platoon testbed[C]// Huisman M, Pǎsǎreanu C, Zhan N. Proceedings of the 24th International Symposium on Formal Methods. Cham: Springer, 2021: 752-762.

[99]

Xue

, Zhan

N J

, Fränzle

, et al. Reach-avoid verification based on convex optimization[DB/OL]. arXiv preprint: 2208.08105, 2022.

[100]

Xue

, Li

R J

, Zhan

N J

, et al. Reach-avoid analysis for stochastic discrete-time systems[C]// Proceedings of the 2021 American Control Conference (ACC). Piscataway:IEEE Press, 2021: 4879-4885.

[101]

Xue

, Fränzle

, Zhan

N J

. Inner-approximating reachable sets for polynomial systems with time-varying uncertainties[J]. IEEE Transactions on Automatic Control, 2020, 65(4): 1468-1483.

https://doi.org/10.1109/TAC.9

[102]

Huang

, Santinelli

, Chen

J J

, et al. Adaptive dynamic power management for hard real-time systems[C]// Proceedings of the 2009 30th IEEE Real-time Systems Symposium. Piscataway: IEEE Press, 2009: 23-32.

[103]

Yan

, Zhu

, Zhang

, et al. Resource-aware design for reliable autonomous applications with multiple periods[C]// Havelund K, Peleska J, Roscoe B, et al. Proceedings of the 22nd International Symposium on Formal Methods. Cham: Springer, 2018: 294-311.

[104]

, Huang

, Chen

, et al. Adaptive workload management in mixed-criticality systems[J]. ACM Transactions on Embedded Computing Systems, 2017, 16(1): 1-27.

[105]

Huang

, Chen

, Buckl

, et al. Conforming the runtime inputs for hard real-time embedded systems[C]// Proceedings of the 49th Annual Design Automation Conference. New York: ACM Press, 2012: 430-436.

[106]

, Huang

, Chen

, et al. Adaptive runtime shaping for mixed-criticality systems[C]// Proceedings of the 2015 International Conference on Embedded Software (EMSOFT). Piscataway:IEEE Press, 2015: 11-20.

[107]

单云霄, 黄润辉, 何泽, 等. 深度纯追随的拟人化无人驾驶转向控制模型[J]. 中国图象图形学报, 2021, 26(1): 176-185.

[108]

Shan

Y X

, Zheng

B L

, Chen

L S

, et al. A reinforcement learning-based adaptive path tracking approach for autonomous driving[J]. IEEE Transactions on Vehicular Technology, 2020, 69(10): 10581-10595.

https://doi.org/10.1109/TVT.25

[109]

Shan

Y X

, Yao

X T

, Lin

H Q

, et al. Lidar-based stable navigable region detection for unmanned surface vehicles[J]. IEEE Transactions on Instrumentation and Measurement, 2021, 70: 1-13.

[110]

Shan

Y X

, Zhou

X M

, Liu

S H

, et al. SiamFPN: A deep learning method for accurate and real-time maritime ship tracking[J]. IEEE Transactions on Circuits and Systems for Video Technology, 2021, 31(1): 315-325.

https://doi.org/10.1109/TCSVT.76

2023年第2卷第1期

PDF下载

1973

1081

引用本文

BibTeX

文章信息

doi: 10.3981/j.issn.2097-0781.2023.01.005

接收时间：2023-01-06
出版时间：2023-03-20
发布时间：2023-03-27

补充材料

相关文章

文章信息

作者

出版历史

收稿日期：2023-01-06
修回日期：2023-02-06

基金

国家自然科学基金(62232008)

国家自然科学基金(62172200)

国家自然科学基金(62032019)

江苏省前沿引领技术基础研究专项(BK20202001)

广东省粤穗联合基金青年基金(2020A1515110199)

深圳市基础研究项目(JCYJ20210324122203009)

深圳市基础研究项目(JCYJ20180508152434975)

作者信息

1.南京大学计算机软件新技术国家重点实验室，南京 210023

2.南京大学软件学院，南京 210023

3.国防科技大学计算机学院，长沙 410073

4.中山大学人工智能学院，珠海 519082

5.广东省大数据分析与处理重点实验室，广州 510275

通讯作者:

^†

参考文献

分享链接

https://castjournals.cast.org.cn/joweb/qzkj/CN/10.3981/j.issn.2097-0781.2023.01.005

分享至

全文二维码

扫描看全文

引用本文

BibTeX

本文的引用情况

表12种不同金属材料的力学参数

科 Family	属数 Number of genus	种数 Number of species	占总种数比例 Percentage of total species (%)	属 Genus	种数 Number of species	占总种数比例 Percentage of total species (%)
鹅膏菌科Amanitaceae	2	11	5.26	鹅膏菌属 Amanita	10	4.78
小菇科 Mycenaceae	2	12	5.74	丝盖伞属 Inocybe	5	2.39
多孔菌科 Polyporaceae	8	14	6.70	蜡蘑属 Laccaria	5	2.39
红菇科 Russulaceae	3	23	11.00	小皮伞属 Marasmius	6	2.87
				小菇属 Mycena	11	5.26
				光柄菇属 Pluteus	5	2.39
				红菇属 Russula	17	8.13
				栓菌属 Trametes	5	2.39

关闭全屏

BibTeX
EndNote
RefWorks
TxT

访问统计

友情链接

联系我们

官方微信公众号