然而，在给软件行为带来精密、高效、快捷等优势的同时，开放不确定场景也给相关软件的设计、实现与可信保障带来了巨大的挑战。以自动驾驶系统为例，其在运行中会采集实时数据来调整自身行为，而这些实时数据中包含周围行人与车辆的位置、运行方向、速度、道路中突现障碍等。这些数据在设计阶段完全无法进行准确预测与描述。在智能制造领域，相关问题同样非常突出，针对实时到达的不同订单，智能车间中的各机器人、机械臂，针对当前具体任务，以及各机器人当前位置、物料分布等情况，实时构建相互之间的组网协作与拓扑关系，并进一步进行行为决策与控制。类似的场景在列控、医疗等任务关键领域比比皆是，已然成为现代软件工作的新常态。在开放不确定，乃至完全未知、未见的场景下，如何保障软件实时行为保持安全，保障软件实时决策的安全精准，对于系统的整体可信保障具有重要的意义，并成为近年来相关研究领域的热点关注方向。对软件系统的正确性进行检测，目前主要有3种基本手段：定理证明、模型检验和软件测试。前两种都需要对软件系统进行建模，在明确外界输入范围的情况下，定理证明采用数学推理的方式，模型检验采用状态遍历的方式对软件系统正确性进行静态验证。软件测试一般采用在一定输入条件下，对比系统输出与标准输出一致性的方法对软件可靠性进行动态检测。与以上3种方法相比，运行时验证（Runtime Verification, RV）主要对运行的软件进行实时监控，根据系统行为是否违背某些规约做出反应。与同样采用形式化方式的模型检验、定理证明相比，运行时验证具有较低的复杂度，可针对系统实时行为进行检验。而与测试相比，运行时验证在对属性进行描述和对程序的监控方面具有更好的灵活性和可扩展性。因此，面向开放不确定环境下安全攸关系统的高可信保障需求，对系统行为进行运行时验证与监控，确保系统安全，并针对各种实时情况做出基于验证的自适应实时响应、决策和动态调控，是相关领域重点关注的研究方向，并取得了一系列进展与突破。本研究将对相关领域国内外进展进行简要分析、总结，并对相关领域研究方向进行展望与讨论。随着计算系统变得越来越复杂，人们逐渐认识到监控的重要性，认为监控是对计算过程（例如进程）中所关心的动态信息进行抽取，并且应该与操作系统的控制管理过程或同步系统的访问仲裁过程中所出现的监控器（Monitor）概念相区分。在电气与电子工程师协会（Institute of Electrical and Electronics Engineers, IEEE）标准中，监控器被定义为“与一个系统或构件并发运行，并对系统或构件的操作进行监督、记录、分析或验证的软件工具或硬件设备”。早期监控方法主要基于跟踪和采样技术并主要用于调试、优化、状态报告、重配置等用途。因此，Snodgrass认为传统监控技术已经不适于监控具有多处理器、分布式特征的复杂系统，同时提出了基于历史数据以及包括数据收集、数据分析和结果显示等步骤的监控过程。人们普遍认为，缺乏集中控制以及在大量不同系统构件（如节点、处理器、进程、内存、地址域等）之间进行跳转是造成复杂系统监控非常困难的主要原因之一，因而构造构件级监控器对分布式系统输入输出和部分状态信息进行监控，然后通过组合技术获取全局监控信息成为一种分而治之、处理复杂性的方式。
监控可以针对系统和软件中的不同侧面，这与应用背景、需求以及用户的关注点相关，并已出现许多相关研究工作。例如，采用不变式或断言对软件运行过程中的变量值、输入/输出或系统状态进行监控；对网络中出现的恶意攻击和非法访问进行监控；以形式规约中提取的事件表达式作为基础对系统的实时性进行监控；通过软件运行时监控技术对无线网络中的能耗进行监测；在面向服务的体系结构（Service Oriented Architecture）中，通过软件封装（Wrapping）技术对Web服务的性能进行监控，以及针对Web服务会话研究运行时监控所需的性质模板等。为了更准确地对复杂时序属性进行监控，以形式化方法为基础的运行时验证得到广泛重视，已被认为是运行时监控的重要研究领域。运行时验证的目标是检测一个系统的实际运行是否违背给定的属性。该属性一般用某种时序逻辑（Temporal Logic）公式描述，并以此为基础生成相应的监控器。因此，在运行时验证中，可将监控器更加具体地定义为“读取有穷运行路径并给出相应结论的装置”。在运行时验证中，线性时序逻辑（Linear Temporal Logic, LTL）作为一种广泛用于描述反应式系统属性的形式规约，获得较多关注和研究。为了增强运行时验证的实时性，可以通过LTL进行扩展来描述实时性质。其中，度量时序逻辑（Metric Temporal Logic, MTL）是一个广受关注的领域，它是在LTL的基础上，通过给时序算子X、U、R等增加时钟实时性质的描述。然而，MTL在密集时间域上的满足性是不可判定的，因此，研究者通过限制MTL语法来得到可判定性，从而产生了MTL的子集度量区间时序逻辑（Metric Interval Temporal Logic, MITL）、定量时序逻辑（Quantitative Temporal Logic, QTL）、信号时序逻辑（Signal Temporal Logic, STL）等。一些学者对MTL这一些子集的可判定性进行了分析，并对其复杂度进行了比较。此外，还有采用时间命题时序逻辑（Timed Propositional Temporal Logic, TPTL）、实时逻辑（Real-Time Logic, RTL）、动态通信自动机（Dynamic Automata with Timers and Events, DATEs）等。为了描述某些更为复杂的需求（如多机器人协同性质、安全性质等），研究人员就这一问题提出了超性质（Hyperproperty）的概念，将形式逻辑语义从单条路径扩展到路径集合。Clarkson等进一步提出HyperLTL的概念，给出超性质在该逻辑下的监控框架。在监控器构造方面，一般由基于约束图、基于逻辑重写和基于自动机3种方式来构造实时性质的监控器。对于基于约束图的方法，相关研究中有代表性的是使用基于RTL的规约语言来表示时间约束的方法。首先通过构造时间约束的约束图，将约束图作为监控器，然后在运行时根据获取到的事件信息，对约束图进行实例化，通过寻找图中是否存在负环来判断性质是否满足。基于逻辑重写的方法在实时领域中研究得更多一些，如针对实时LTL和MTL的基于逻辑重写的验证方法。该方法以on-the-fly的方式将性质公式重写为正则形式，通常通过逻辑的不动点刻画来实现，运行时只需保存下一状态需满足的公式。近年来，基于自动机理论根据实时时序逻辑构造时间自动机（Timed Automata），并将时间自动机的扩展形式作为监控器，也是一个重要方向。除上述监控方法外，还有不少相关的研究工作，受限于篇幅，在此不再一一阐述。上述验证方法多基于逻辑的两值语义，有时不能尽早地发现性质背离，而这一点对于监控实时性质来说非常重要。Leucker等对基于TLTL三值语义的运行时验证进行研究，扩展了LTL的标准语义，增加了表示“不确定”的状态“？”，釆用事件时钟自动机作为监控器形式化描述，通过求性质公式及其取反公式的相应事件时钟自动机的笛卡儿积，得到三值语义监控器，监控过程中采用符号化执行的方式来判定系统执行是否满足或违背性质规约。在信息不完善的情况下，三值语义能够更明确地进行表达。此外，Bauer等提出的RV-LTL为四值语义，其对不确定状态的LTL属性可进一步进行可能为真或者可能为假的推测。近年来，对人机物融合系统进行运行时验证越来越受到重视。例如，Mitsch等将定理证明合成监控器的方法用于信息物理融合系统（Cyber-Physical System, CPS）的运行时验证；Fraigniaud等利用去中心化思想将RV运用于分布式系统的监控；Pedro等利用MTL语言实现对实时系统的监控；Singh等将STL用于CPS的软件测试。随着无人系统更加广泛地应用于民生和国防各领域，采用运行时验证技术对无人系统进行监控的相关研究也相继出现。例如，Kane等利用独立硬件实现对自主驾驶系统的运行时验证，Aiello等利用运行时保证技术实现对关键飞行控制系统的监控。除了CPS，RV在商业软件方面也有广泛的应用前景，例如Luo等利用RV进行云服务工作流时序的一致性检测等。RV关注于已经发生的轨迹分析与监控相似，而近年来在线验证（Online Verification）思想也被提出，并得到广泛关注。其基本思想是在线获取系统运行时参数来构建系统模型，然后基于模型检验方法尽可能高效地验证系统在后续有限时间内的安全性。为实现在线监控，Johnson等、Chen等提出了基于集合的线性混成系统在线可达性验证方法。Chen等还通过对非线性混成系统进行简化，将已有方法扩展到非线性系统的在线监控。在监控器生成和部署后，虽然以在线实时的方式能够得到性质的满足与违反判定结果，但在安全攸关系统中这还并不足够。为了在运行过程中自动化地及时发现安全性恶意行为并进行相应控制防护，最早在2000年，由Schneider提出了将传统运行时验证、控制、增强等手段相结合，自动生成安全代码，以弥补运行时验证理论在动态环境不确定因素方面防护能力的欠缺。
与运行时验证的区别是，除了可以对软件在运行时的非正常行为进行监控，当异常行为发生时，还可以采取一些增强措施来保持某些关键安全性质，即软件运行时增强（Runtime Enforcement, RE）技术。运行时增强方面的研究最早开始在安全自动机上开展，其原理是通过强制监控器监控当前执行序列是否违背期望性质，如果监控到违反，可以通过立即中止程序运行的方式来避免重大的安全问题。此后，又有了大量的对增强机制的研究，以及对可增强属性的探索，将属性范围拓展到除安全性质以外更广泛的应用中，并提出了更加强大的安全防护代码模型，也出现了运行时增强工具等，可以将安全约束属性转换为安全增强监控代码。程序在执行任何安全相关操作的上下文时，监控器可以通过插入其他动作，如抑制动作（停止、替换、插入等），或允许输入动作序列不受干扰地执行，促使软件按照安全的行为序列运行。运行时增强过程如图1所示。在这样一个作用过程中，系统允许进行插装，以即时验证待执行操作是否违反安全性质的监控器，并且允许插入或抑制操作来保证系统的输出始终符合性质，其中的输入操作序列由用户或原系统执行产生，输出序列被发送到安全防护的监控器（也称为强制防护器或防护器）。如图1所示的一个运行时增强过程是一个在系统运行时对Π属性进行防护的决策过程。它读取一个有限（可能是无限）的事件序列σ，然后输出一个新的有限（可能是无限）的事件序列o。安全防护的监控器配备了一个内部存储区和一组对输入事件的操作（时序性质相关的数据可能需要存储）。增强过程是作用于σ与o之间的一道防护。为了保证防护方法的合理有效，σ与o之间可能还存在一些约束（如透明性）等，从而影响读取输入事件序列σ时防护监控器所采取的强制操作。因此，在构造运行时增强监控器时需要遵守透明性（Transparency）和可靠性（Soundness）的原则。其中，透明性是指运行时强制方法构造的安全性质防护器在全过程中不应妨碍原系统中正确的执行序列；可靠性是指被防护系统中的不正确执行序列必须被阻止或纠正。除了以上两则约束以外，研究者还总结了一些强制方法中应该尽量考虑的特性（表1），使得强制方法更加优化。表1 运行时增强技术中应考虑的特性
近年来，软件运行时增强技术的研究取得了长足发展。Lanotte等针对工业控制系统所面临的安全问题，提出了基于运行时增强的形式化方法来增强网络控制器的安全性。Pinisetty等面向CPS的可靠性问题，提出了心脏起搏系统的闭环运行时增强框架。Hu等提出的面向机器人系统的运行增强框架，增强了机器人集群在不确定环境下运行时的安全性。
前文从运行时验证、监控和增强的角度对相关工作的整体思路进行了介绍。下文将以工作于开放不确定场景下的实时系统（如自动驾驶、列车控制等）为代表，对软件系统面向外在环境、内在行为的不确定性所开展的建模、验证，特别是动态调控方面的工作进一步展开讨论。
开放不确定场景下软件运行空间充斥着诸多“不确定性”，而这个“不确定性”是贯穿感知—预测—规控上下游的，主要体现在感知局限性，例如车载硬件的感知能力是有局限的，激光探测及测距系统（Light Detection and Ranging, LiDAR）的可靠感知范围不过百米，货车等大型交通参与者也会造成视角遮挡等。忽略这些不确定性的影响进行规划，将导致规划的轨迹不再具有安全的属性，使系统产生不安全行为。为保障行为安全，构建不确定性环境的概率模型，并在此基础上自适应规划概率安全的轨迹是当前的一个主要方向。规划概率安全轨迹的前提是准确构建环境概率模型。环境中往往存在多种运动模态、形状各异的物体。为了能够准确估计物体的位置和形状信息，需要充分地利用有限的历史观测数据，通过一种基于概率分析的环境构建方法对机器人当前的未知外部环境进行统计分析。在此基础上，轨迹规划方法传播系统的位姿不确定性与环境的概率模型进行交互计算，以映射不确定性到规划的轨迹。在以上规划过程中，环境建模的精度和规划算法的效率问题是两个重要的问题。粗糙的建模过程将导致规划的轨迹过于保守，低效的规划过程不利于实现实时计算而失去规划的实际意义。面向实际的机器人系统规划需求，实现高精度的环境建模和实时的规划是两个必须深入考虑的问题。实现高精度的环境建模需要从环境中物体的形状和位置两个对规划非常重要的属性分别进行建模。一方面，利用传感器感知的物体形状是随着时间维度不断完善的过程，因此需构建动态的建模方法，通过数据的不断补充实现物体形状的精确建模；另一方面，动态的物体位置预测需考虑多方面的影响，包括物体的运动倾向、运动模型、环境约束等。多种约束的存在应使建模的方法具有较好的拓展框架，可兼容多种约束的影响。在环境建模的基础上，高效的位姿不确定性传播以及与环境模型的交互计算方法是提高规划算法效率的关键。此外，规划过程需要考虑轨迹的质量问题。基于此，规划算法的研究应首先着眼于交互计算方法的优化，然后在规划框架方面体现优化的过程。当前处理不确定性的方法主要有概率统计理论、模糊理论、粗糙集理论和灰色系统理论等，其中概率方法主要研究随机不确定性信息的描述与表达，理论最为完善，方法最为成熟，是当前移动机器人研究的主流方法。Barth等的卡尔曼滤波和蒙特卡罗方法在短距离不确定性的预测场景下可获得较好预测性能。Houenou等对角速度和加速度进行预测，提高了长时预测的性能。刘志强等采用传统机器学习方法对运动轨迹进行预测，如隐马尔可夫模型和支持向量机等。李建平等结合了隐马尔可夫模型和高斯混合模型对车辆历史轨迹进行建模，在较为简单的驾驶环境中取得了较高的预测精度。不确定条件下的规划过程可被构建为一个部分可观测马尔可夫决策过程（Partially Observable Markov Decision Process, POMDP），机器人从一个不可被完全观测的状态向下一个状态演化，规划的目的是求解控制策略以实现从状态的概率分布到机器人行为的映射过程。基于这个过程，一系列基于求解POMDP的方法被提出以实现多种应用。例如，不确定环境下的无人驾驶、移动机器人等。尽管基于POMDP的方法已经在理论和实际实验中显示出了较好的成绩，但求解POMDP的计算效率问题仍旧难以解决，尤其是考虑高动态的环境下，无法实时计算的算法难以跟上环境的变化。为了简化计算难度，另外一种处理不确定性的方法将该类问题转化为求解机会约束优化问题。Blackmore等针对威胁的不确定性，提出了基于机会约束的路径规划方法，虽然这种优化已被证明可用于实时路径规划，但它在复杂和动态环境中可扩展性较差。Zhu等将机会约束和模型预测控制结合在一起，在滚动优化的框架下实现机会约束的求解以确保在存在感知和定位不确定性的条件下多个无人机之间无碰撞。Arantes等针对如何平衡不确定性条件下的规划问题和安全问题展开了研究，通过确保机器人在连续2个时间步之间的安全性满足机会不等式约束。这些利用机会约束优化的方法从多个维度对机会约束优化的算法展开了研究，然而这些算法大多只在仿真环境下应用，对于如何平衡实际机器人需求的效率、安全、优化等问题仍没有很好的解决方案。开放不确定场景下软件行为中离散跳转与连续行为紧密交织，这样的特性决定了混成自动机（Hybrid Automata, HA）是其最自然的建模语言之一。目前，对混成自动机的建模与验证研究主要集中在混成自动机的安全性（Safety）检验上，其直观概念可以解读为系统运行中是否会发生不好的行为。安全性检验，即检验从给定的初始条件出发，系统运行中是否会出现违背规约或者不安全的行为。由于混成自动机的运行既包含状态的离散变化，又包含状态的连续变化，其相应的模型检验问题十分困难。目前对混成自动机的模型检验主要集中在安全性的一个子集——可达性（Reachability）问题上。
与可达性验证有所不同，混成系统的控制问题旨在找到一组系统外部的控制输入和系统的控制模式序列，使得对应的系统行为能满足系统内部和外部环境的所有安全性约束以及特定的控制目标。要完成混成系统的最优控制生成，就是要找到尽可能最优的外部控制输入和控制模式序列。对于可微混成系统，主流的控制生成方法是基于梯度下降的。Xu等首先提出了经典的基于梯度的双层优化算法，在顶层生成控制序列，在底层基于梯度优化求解最优外部输入。在此基础上，Egerstedt等基于最速下降法来加速底层外部输入的优化求解过程，CaldWell等、Johnson等则是使用基于梯度下降法来加速底层优化求解。除此之外，Gonzalez等、Ali等也设计了各种算法来加速顶层控制模式序列的优化求解过程。除了主流的基于梯度的可微混成系统控制生成方法，Nilsson等和Ding等也提出了一些基于数值计算的控制生成方法。对于不可微混成系统，由于梯度信息难以获取，主流的控制生成方法是基于采样和各种启发式搜索来进行控制生成。例如，Branicky等基于路径规划中的快速扩展随机生成树（Rapidly-exploring Random Trees, RRTs）算法进行控制生成，但缺少最优性的理论保障。此后，Farahani等提出了一种鲁棒的稳定模型预测控制生成（Model Predictive Control, MPC）方法，基于蒙特卡罗模拟拒绝采样（Monte Carlo Simulation and Rejection Sampling, MCRS）来解决最坏情况下的MPC控制问题，不过其处理复杂控制任务的能力相对有限。如何对给定的混成系统快速高效地生成控制参数仍是一个亟待解决的问题。上述验证与控制方法通过在系统运行前形式化地验证系统安全性，来保障系统运行时的安全。然而，对于实际问题中规模极大、复杂性极高、系统环境参数在运行时才能确定的软件系统，上述验证与控制方法难以在系统运行前完成对其安全性的验证。因此，Sha等提出了Simplex的架构思想，即通过系统在线监控使得系统在高性能但不保证安全的控制策略与低性能但已被验证安全的控制策略间切换。例如，一旦在线监控预测到了系统某一安全性质即将被违背时，则将系统控制策略切换成安全的备用策略。系统在线监控能否及时有效地预测到系统的不安全行为是该Simplex架构的关键。近年来，基于在线验证对于系统实时行为进行快速在线建模，并对状态安全性进行验证也是相关领域的一个重点关注方向。Pek等通过在线验证对自动驾驶的运行时安全进行验证并进行干预来保证系统运行安全。在上述运行时验证、监控、增强、动态调控等领域，国内学者也进行了长期的研究与探索，并取得了系列进展与成果，选取其中部分工作介绍如下。
（1）在基于运行时验证的软件监控方面，国防科技大学团队围绕如何在系统错误发生之前进行预测并开展长期研究。他们提出在系统运行前即提取出被监控系统的模型以及根据属性规约来自动产生运行时监控器，运行时阶段，将当期系统执行路径所需要的前瞻信息从模型中收集，以判定未来执行路径是否将违背被监控的属性和规约，在此基础上进一步提出了基于程序代码的静态分析方法来辅助运行时监控的预测。此外，他们提出在运行时对代码段进行分析，从而得到辅助信息来进行预测，对于复杂系统来说，这无疑更有可取性。南京航空航天大学团队研究了内存安全性和形式化规约的运行时监控技术：在内存安全性方面，提出了基于智能状态的监控算法和源代码级别的插桩框架，并实现了工具Movec；在形式化规约方面，提出了C程序参数化运行时验证算法，证明了参数化运行时验证的时间复杂度是NP完全的，提出了规约的四值可监控性概念及其判定算法。（2）在基于运行时验证的软件调控方面，南京大学在混成系统在线验证与控制方面进行了长期探索。针对CPS在开放不确定场景下的动态行为监控问题，南京大学团队提出了面向带参混成自动机的安全攸关场景驱动在线验证方式。通过对系统后续短期状态空间进行在线快速前瞻式验证，发现风险并提前进行预警。此外，相关团队研究了基于无梯度优化的混成系统控制生成方式，使得对复杂混成系统在线生成控制参数成为可能。在此基础上，进一步提出了将在线验证与控制生成相结合的运行时安全保障方法，当在线验证发现后续潜在风险时，在线生成安全控制参数，接管系统行为，从而形成一个可以对动态系统后续状态空间在线验证，并对潜在危险进行预测、反馈与干预的新型在线容错方法，保障系统运行安全。相关工作已经在轨道交通、智能制造、智能驾驶等领域展开实例研究。中国科学院软件研究所（简称软件所）团队在（随机）混成系统安全性验证方面取得突破，尤其在可达-规避分析方面做了大量理论研究，例如构建了刻画可达-规避集合表达能力强的凸约束。基于这方面的研究，以及当前智能驾驶等安全攸关系统的需要，软件所团队也开展了基于可达-规避分析的安全控制律生成的研究，通过提出高效的（鲁棒）约束求解算法来有效地生成安全控制率，服务于安全攸关系统（如智能驾驶）的实时控制。（3）针对CPS中的扰动信号及不确定环境，华东师范大学基于STL，增加刻画扰动信号的算子，提出能够刻画扰动范围的扰动信号时态逻辑（Perturbed Signal Temporal Logic, PertSTL），并提出一种面向PertSTL的在线检测方法，从而帮助分析一定范围内的信号扰动对验证结果产生的最坏影响。该方法已成功应用于汽车自动驾驶场景、智能建筑的温控系统的在线检测，能有效分析信号扰动对系统安全性的影响。（4）在系统级层面，中山大学无人系统团队在混合关键级系统方面做了许多理论研究工作，特别是在面向最坏情况执行时间（Worst-Case Execution Time, WCET）的运行时监控和自适应调整方面，包括形式化验证、在线监控、自适应调整等方面，提出了包括自适应能量管理、自适应工作流管理等先进方法和理论，服务于无人系统的实时在线运行。此外，团队在应用于实时系统的规划和控制方面进行了较为深入的研究工作，并应用到了无人驾驶车辆规划、转向控制、水面自主航行可通行区域建模、海面目标跟踪等领域，取得了显著的效果。通过对近年来国内学者在基于形式化建模与验证等手段的复杂软件在线监控等领域的部分代表性工作进行总结（事实上在更广泛的自动控制领域还有着大量工作，囿于本文主题所限，未在文章中进行整体总结），可以看出国内学者在软件运行时验证、监控、动态调控等方向的理论、算法、工具等方面均取得了一系列显著的进展，并且已经在轨道交通、智能制造、无人车、无人船等领域进行应用验证。如何进一步推动相关研究，特别是面向智能时代下复杂软件所面临的挑战，形成开放不确定场景下软件运行时验证、监控、与动态调控的方法与体系，有待相关领域产学研深入协作与研究。通过对运行时验证、监控、增强及动态调控等方面的国内外研究进展的介绍与总结可以看出，相关领域得到了国内外专家学者的广泛关注与持续研究，并取得了系列重要成果。然而，随着“开放不确定”这一关键词成为轨道交通、航空航天、智能驾驶、智能制造等国家重要战略发展领域软件运行的新常态，并且伴随着智能化浪潮带来的巨大变革，相关领域仍有大量工作亟待解决。关于中国在该领域的后续研究，提出以下几点建议。
（1）面向开放不确定环境的概率建模与轨迹规划。概率化建模软件运行环境中物体的位置、分布等信息，使软件对所处环境进行充分理解，并进行在线快速路径规划与调整，以保证系统运行安全，是面向开放不确定场景挑战的重要方向之一。（2）面向实时动态行为的软件行为建模与控制生成。在静态建模语言方面进行拓展，分别在动态参数、动态交互拓扑等层面进行参数化描述与运行时模型实例化，准确刻画系统实际行为，以帮助后续运行时监控与验证实时、准确捕获当前系统行为，是有效在线监控的必由之路。（3）面向安全容错的软件行为控制器自学习。由于系统行为中各种动态行为高发，传统的基于正向推导的离线静态设计方法难以对相关复杂系统生成安全控制逻辑。基于智能化学习技术构建安全可信的系统控制器，是相关领域近年来的重点关注所在。（4）面向黑盒不可解释系统的运行时监控与调控。当前各类信息物理系统中包含越来越多的智能组件，如神经网络模型等，其结构复杂、参数众多，难以对其具体行为和决策进行解释，为了确保这些组件运行结果的安全性和可靠性，对其行为进行运行时监控和调控非常必要。（5）覆盖软件运行全生命周期的运行时监控与反馈。从软件系统架构角度研究一种新的系统设计方案，将基于在线验证与控制的系统容错机制纳入系统设计，使得运行系统与监控模块间可以无缝交互，保障系统运行，具有重要意义。在开放不确定场景下，软件与外界密切交互，主动感知并构建外界环境与自身行为模型，实时形成控制策略并快速执行，以期提供及时、精确且安全可靠的服务。面向相关高度动态、不确定行为，对其进行准确的形式化建模、验证与监控，并进行动态调控是保障相关软件准确、高效运行的重要手段。在此基础上进一步研究并形成完整的复杂软件系统运行时可信保障技术与方案，开发有效的运行时验证、监控、调控等工具，并服务于轨道交通、航空航天、智能驾驶、智能制造等国家重要发展领域，具有重要研究意义与应用前景。
