通过AI支持的CPS的I/O痕迹的混合自动机挖掘实现操作安全验证

版权归作者所有。通过使用AI支持的CPS的I/O痕迹的混合自动机挖掘实现操作安全验证Imane Lamrani，Ayan Banerjee和Sandeep K.S.古普塔冲击实验室，CISDE，亚利桑那州立大学，坦佩，亚利桑那州{ilamrani，abanerj3，sandeep.gupta} @ asu.edu摘要人工智能使能的网络物理系统，如人工胰腺，遭受该系统受到在训练时间期间未观察到的输入和场景的影响，因此预期输出是未知的因此，在部署之前使用预测模型来表征控制系统的行为的流行的基于模型的验证技术在这项研究中，我们提出了一种操作安全验证技术，通过混合系统挖掘部署的AI启用的网络物理系统的输入/输出跟踪。混合自动机模型使形式化验证的安全性，尽管我们将我们的技术应用于人工胰腺控制系统，利用人工胰腺系统门诊研究的数据。我们证明了我们的技术成功地推断出这些系统在该领域的准确的混合自动机表示，并可用于执行安全分析，以确定安全的系统中存在的输入和方案的预期输出的系统是未知的。我们确定了一个评估方案，其中存在明显的安全违规行为。1介绍人工智能（AI）和机器学习（ML）在安全关键型网络物理系统（CPS）中的应用越来越多，最近的致命故障案例重新引发了对认证问题的讨论，并迫切需要开发严格的安全验证技术。然而，操作组件交互环境、人工智能CPS中的人在回路中的包含以及环境变化使得正式的安全验证成为一项非常具有挑战性的任务。传统的安全验证方法涉及测试和模拟，不再足以评估启用AI的CPS的安全性，其中需要进行详尽的安全验证。相比之下，形式化的方法，如模型检查，以克服传统的安全验证技术的局限性。然而，这些方法可能达不到AI使能CPS，其中完整的正式验证模型通常不可用。因此，现实世界中启用AI的CPS操作倾向于偏离系统的安全保证设计。人工智能支持的CPS，如人工胰腺（AP）或自动胰腺，正在使用机器学习来做出几个关键决策。例如，让我们考虑Medtronic 670G AP（闭环血糖控制系统）的血糖预测系统。该系统使用预测模型来预测低血糖水平。如果预测血糖水平在未来将较低，则输注泵关闭。目的是避免可能导致致命后果的低血糖。然而，如果预测是错误的，它可能导致高血糖，这对身体有长期的负面影响模型预测取决于人类用户的生理参数，例如胰岛素敏感性。这些参数取决于人的行为，如身体活动，饮食模式和精神状态。这种参数变化在设计控制系统时无法复制。在本文中，我们提出了一种新的方法，如图1所示，以解决给定的问题，基于模型的安全验证的人工智能启用的网络物理控制系统与有限的预言。我们的方法最初considers一个混合系统表示的控制系统，描述了预期的操作，系统进行了测试，验证，并使用控制实验研究验证。然后，我们描述了一种方法，从输入/输出（I/O）时间序列数据中挖掘支持AI的控制系统的混合系统表示。如果开采的混合系统与制造商提供的文件中定义的初始混合模型相同然而，如果所挖掘的混合系统不同于最初表达的混合系统（关于模式的数量、流动动力学、模式转换、保护条件或重置条件），则安全结论可能会发生重大变化。在这种情况下，我们考虑对新开采的混合系统进行可达性分析，以评估控制系统的安全性（Mr.1995年）。如果新挖掘的混合系统是不安全的，则可以潜在地调用根本原因分析算法。我们不讨论这个问题在我们的论文中，但肯定是一个未来的努力。此外，安全关键CPS在上市前应符合政府监管要求。由于生产压力和相互冲突的目标和权衡，或-版权所有© 2020本文由其作者。在知识共享许可署名4.0国际（CC BY 4.0）下允许使用。学习HA和评价产出HA挖矿工具警卫采矿流动方程提取控制模式分类输入/输出轨迹分割HA挖矿工具输入制造商AI使能CPS非确定性oracle输入1. 系统规范2. 操作输入/输出跟踪安全启用AI的CPS。不安全•探测到入侵•需要额外的操作跟踪•规格中未披露重要信息。图1：拟定安全性验证技术的总体方案。组织往往会通过放松保障和控制而进入高风险状态（Leveson 2011）。例如，大众汽车的失败装置允许车辆在监管测试期间 不正确地“ 系统的设计目的”、“操作员认为系统在做什么”和“系统实际在 做 什 么 ” 之 间 的 不 协 调 最 终 报 告 （ 编 号 ：KNKT.18.10.35.04）称，这是导致波音Max 8致命坠机的复合因素之一。这个问题对于具有人工智能或自适应组件的工业4.0系统来说变得更加重要和具有高度挑战性，其中系统是灵活的，完全自主的，并且在遇到新情况时调整其模型。这激发了对严格的操作安全验证技术的需求，以帮助监控和维护系统在现实世界中的安全操作。本文通过结合信息论、形式化方法和机器学习来解决这个问题，以获得一种主动的操作安全验证技术，该技术一旦部署到现场，就可以检测到人工智能CPS安全保证设计的有意或无意偏差 本文的组织结构如下：第2节讨论了解决所讨论问题的竞争工作，第3节讨论了与AI启用的系统模型相关的定义和分类，第4节提供了有关所提出的技术的详细信息，第5节评估了所提出的提取混合自动机的技术的有效性，最后第6节总结了本文。1https://www.flightradar24.com/blog/wp-content/uploads/2019/10/JT610-PK-LQP-Final-Report.pdf2相关工作2.1工程安全关键系统验证支持AI的CPS的安全性和正确操作依赖于验证软件和物理环境之间的正确交互（Leveson 2011）。Leveson使用系统理论过程来识别安全约束，这有助于设计或重新设计更安全的系统。这些技术通常应用于复杂安全关键系统的设计阶段。它们也可以用于事故的根本原因分析。具有人工智能（AI）和机器学习（ML）组件的安全关键型CPS的形式化设计和验证Dreossi等人提出了一个工具包VERIFAI，该工具包专注于对基于AI的系统进行基于仿真的安全分析，其中使用了系统的可仿真抽象模型。在这项工作中，我们希望确定使用从启用AI的CPS的真实世界操作中收集的痕迹学习的安全验证结果与正式或模拟的安全验证结果一致。另一方面，可达性分析是一种正式的安全验证技术，在文献中针对时不变系统进行了广泛的研究（Wendr等人，1995; Frehse等人，2011; Fan等人，2016）。它确定了系统从一组有界初始条件开始时可能访问的状态集。如果没有不安全状态可达，则系统可以被认为是安全的。在这项工作中，我们提出了一个安全验证计划，旨在以积极主动的方式在现场（在操作阶段）该方案是基于混合自动机使用从现场启用AI的CPS的操作中收集的实时数据进行挖掘。我们应用可达性分析的学习混合自动机，以验证操作AI启用CPS的安全性。2.2挖掘混合自动机以前的一些工作已经提出了学习混合自动机的算法和框架。Minopoli和Frehse提出了一种将simulink模型转 换 为 混 合 自 动 机 的 工 具 （ Minopoli 和 Frehse2016）。Lyde和Might提出了一种使用抽象解释分析控制代码并从抽象状态转换系统推断混合自动机的方法然而，我们的工作不同之处在于，我们学习混合自动机模型自动使用系统操作的I/O痕迹。从I/O轨迹中挖掘HA：Medhat等人提出了一个框架，用于仅使用执行轨迹从黑盒系统中挖掘粉状自动机。此框架仅限于以以下形式展示输入更改的系统：假设这些变化在输出轨迹中具有瞬时效应，这在实践中并不常见（Medhat等人，2015）。此外，作者仅将保护条件视为基于时间的转换，因此无法使用他们提出的框架对输出值的保护进行建模。Balakrishnan et.al提出了一种仅使用系统的连续输 出 来 确 定 最 大 似 然 混 合 系 统 模 型 的 算 法（Balakrishnan et al.2004），但这项工作假设保护条件与连续状态无关，这限制了可以使用所提出的技术学习。Blackmore et. al通过包括以连续状态为条件的自主模式转变来扩展这项工作，但是他们的方法假设给定了保护条件（Blackmore等人，2007）。我们提出的混合自动机挖掘技术通过连续状态的聚类来获得保护条件。Ly和Lipson提出了一种使用聚类符号回归的方法，一种机器学习算法，用于从未标记的时间序列数据中推断非线性符号表达式，该表达式对动态系统的行为进行建模（Ly和Lipson2012）。作者还提出了一个过渡建模算法，搜索非线性符号不等式模型的保护条件。与我们提出的技术不同，他们的工作假设保护条件与系统输入的变化严格相关，并且系统不能有两个具有相似行为的不同模式。此外，系统的行为被定义为严格的I/O关系，而不是我们的混合挖掘技术，其中行为由微分方程表示。此外，与我们的技术相反，一些相关方法需要离散模式数量的先验知识（Santana et al. 2015;Ly and Lipson 2012）。尼格曼等他们对混合系统的行为模型的自动学习和学习模型的应用具有相同的动机，以检测整体系统行为中的异常（Niggemann et al.2014; Niggemann and Lohweg 2015 ） 。 另 一 方 面 ，HyBUTLA（尼格曼等人2012）推断混合时间概率自动机，而我们的技术放松了这种时间约束，这允许它推断更大类混合系统的混合自动机模型。CHARDA是最接近我们的工作，并被应用于学习视频游戏角色的混合行为（Summerville，Osborn和Mateas 2017）。然而，我们提出的技术和CHARDA的不同之处在于，CHARDA仅限于连续状态变量的导数为常数的系统，这在实践中往往无法观察到。在这项工作中，我们采用了混合自动机挖掘技术HyMn（Lamrani，Banerjee和Gupta 2018），并采用了一种新的流提取技术，其中采用多变量非线性多项式回归分析来推导非线性动态演化。此外，我们通过第4.1节中讨论的RuLSIF技术更新了HyMn算法中这种重新分类的输出是启用AI的CPS的独特模式。2.3一致性测试我们提出的方法与验证运行的CPS及其所需行为的正式规范之间的一致性具有相同的动机，一致性测试（Woehrle，Lampka和Thiele 2012; Abbas 2015）。Woehrle等阿尔介绍一种一致性测试方法，它依赖于将系统的规范及其实现生成的跟踪映射到时间自动机，并验证每个生成的实现跟踪是否包含在规范时间自动机的跟踪中。然而，他们的方法仅限于时间自动机类。与这种一致性概念相反，其他作品将一致性测试定义为实现与规范模型之间的紧密度度量，其计算仅依赖于系统跟踪（Abbas 2015; Araujo etal. 2018）。然而，即使对于简单的线性系统，提供关于一致性程度的保证仍然是一个挑战。最后，据我们所知，一致性测试方法的输出仅限于通过或失败。因此，在一致性失败的情况下，仅向测试工程师提供调试跟踪，这有助于调试CPS的实现错误。对于复杂的系统，在没有操作模型的情况下定位根本原因可能需要大量的工作。新颖性：本文提出的HA挖掘算法与相关工作的不同之处在于以下关键因素：• 它可以提取控制模式，其中控制器输出是连续状态变量的线性组合，• 连续状态变量遵循一组非线性微分方程。3定义和分类3.1系统模型支持AI的CPS是一个系统，包括感知组件，规划器/控制器和环境发生低血糖/高血糖事件。这些危险事件是由于胰岛素的不准确输注而发生的，例如，如果葡萄糖浓度G超过180mg/dl，则其可能导致高血糖症，而低葡萄糖水平，即，低于60mg/dl可引起低血糖。AP的动力学由非线性方程1表示，2和3，其中X代表的变化率在图2：非线性人工智能支持的网络物理系统。（system under control）（Russell and Norvig 2016）.如图2所示，启用AI的CPS与间质胰岛素浓度，G是输注胰岛素浓度X时血糖浓度（G）的变化率，I是血浆胰岛素浓度（I）的变化率（Andersen and Højbjerre 2002）。AP设备有三种控制模式：1-基础，其中重置条件It= 5，2-制动，其中It= 0。5 G +44。75和3-校正推注，其中It= 50。表达血糖和血糖水平的微分方程环境中使用一组传感器和执行器。 的环境可以使用一组n个连续变量{x1，x2，. . . ，xn}。连续变量由一组非线性微分方程控制，这些方程也由p个控制输出{o1，o2，. . .，p}。连续变量状态作为输入提供给对物理环境执行动作的代理，以便使用环境的当前和预测状态来实现给定或计算的目标。当前状态 并且3.2操作安全操作安全性是确保人工智能CPS在现场的操作不会偏离系统的安全它旨在检测系统系统的实际工作和操作员认为系统的工作之间的这种不协调可能是由于有意的破坏情况（由于生产压力或目标权衡）或无意的破坏情况（要求、规范、设计或实施中的缺陷）。在其开发生命周期中比如说胰岛素相互作用本质上是非线性。Xstec=-k2。X（t）+k3. （I（t）−Ib），（1）Gstec=−X（t）。G（t）+k1。（Gb−G（t）），（2）Istec =−k4. I（t）+k5. （G（t）−k6）+.t.（三）3.4非线性混合自动机AI使能系统是包括与连续动态系统（非线性物理环境）交互的离散转换系统（智能代理）的动态系统。非线性混合自动机是结合离散演化（控制模式转换和变量更新）和连续演化（由微分方程控制的系统动态）的闭环系统的模型我们正式定义了一个非线性混合自动机形式模型的AI启用CPS如下。混合自动机：混合自动机H是元组其中：• X={x1. . . xSm}是连 续 变 量 的有限集合，其中X=10。I是一组内部输入变量，O是一组输出（受控）变量。 在变量集X上的一个值是Rm的一个成员，使得每个变量xi∈X都是一个实值。Xstec={xstec1，. . . ，xstecm}是点连续变量的集合表示连续函数的一阶导数变量在不断变化。X ′={x′，. . . ，x′}1m大众汽车系统对潜在的危险情况。是一组带初始值的连续变量，它表示控制模式转换结束时的变量值。• M={m1. . . mn}是控制模式的有限集合。• 集合Fmi 非线性常微分方程在XSX范围内，表示动态演化（流3.3人工智能支持的CPS示例：人工胰腺（AP）AP控制系统是用于自动控制1型糖尿病患者血糖水平的AI启用CPS代理提前30分钟使用预测的葡萄糖水平，并输出适当量的胰岛素输注速率It，以使输注泵在接下来的30分钟内保持代理商速率）的每个变量xi对于每个控制模式mi∈ M。• E是一个有限的边缘集，称为模式转换或模式变化。每一条边ei∈ E由保护条件Gmi，mj和重置条件Rmi ，mj的合取定义，其中mi∈M是源模式，mj∈M是目标模式.• 保护条件Gmi ， mj是X 中 变 量 的线性多面体约束。mi之间的过渡输入走线传感器系列2电流状态制造商规范文件安全基于HA挖掘技术的验证执行器1行动决定输出走线剂基于目标的Agent程序环境模型预测状态非线性环境DT并且当连续变量集X∈Gmi，mj的值时，使能跟随边缘e i的m j。G是所有保护条件的集合• 重置条件Rm，m，由线性分配给出3.6符号R是实数的集合。xs t e c和dx都表示x相对于t的差。变量列表X上的多面体约束是有限的SIX中的变量j′X，关联一个变量赋值-X上线性约束的合取。沿着边缘进入模式转换mi到mjei，例如x′=xi，其中x′表示更新后的变量列表X上的线性约束被定义为形式P（X）r的表达式，其中P（X）是多项式，X上的i im ial项，r∈R，且n∈{≤，≥，>，=}。在边ei被遍历之后变量xiR是所有复位条件的集合。3.5假设提出的基于HA挖掘的安全验证技术要求制造商提供系统的参考安全保证（认证）混合自动机模型。然而，制造商可能无法提供混合自动机作为我们的安全验证技术的参考规范模型，因为他们可能使用了不同的规范模型，如i*、UML、SysML、MARTE、Agent UML。然而，从规范文档中学习混合自动机模型或将给定的规范模型映射到混合自动机模型是可行的（Burmester，Giese和Oberschelp 2006; Schmitz etal.2009; Liu et al.2013年a）。例如，对于飞机等安全关键控制系统，需要模拟器进行操作员该模拟器可用于我们的技术作为参考规格模型。对于人工胰腺，UVA/Padova是FDA批准的模拟器，并且已经在研究中大量采用，作为某些胰岛素治疗的临床前试验的替代，包括测试AP的闭环控制算法（Man etal.2014年）。因此，将人工胰腺的控制逻辑与模拟器相结合可以代表Medtronic 670G的参考规格Simulink模型。此外，一些先前的工作已经提出了算法和框架映射一些形式化模型到一个混合自动机。例如，Minopoli和Frehse创建了一个工具，用于将simulink模型转换为混合自动机（Minopoli和Frehse 2016）。Lyde和Might提出了一种使用抽象解释分析控制代码并从抽象状态转 换系统推断混合自动机的方法（Lyde和Might 2013）。所提出的技术的另一个假设是迹线是无噪声的。然而，大多数CPS具有信号处理和滤波算法，以确保控制逻辑仅使用高质量的传感数据。因此，CPS的控制器使用经过滤、调整和校准的数据来做出决策。然而，如果预滤波、滤波或校准不作为传感器发射器的一部分，则从传感器收集的数据可能不被处理在这种情况下，我们提出的方法假设在规范文档中提供了预滤波、滤波或校准方法（因为它是控制器的一部分）。因此，这些模块是隐藏控制变量的一部分，如果我们有它们的规范的描述，那么我们可以很容易地模拟处理的数据。2https://www.bloomberg.com/news/articles/2019-11-08/delays-in-boeing-max-return-begin-with-near-crash-in-simulator4基于HA的安全验证方法我们提出了一种安全验证算法，该算法基于非线性AI启用CPS的逆向工程，来自从CPS现场操作和制造商提供的系统规范（初始HA）中收集的操作时间序列轨迹。所提出的安全验证技术的方案如图1所示。• HA挖掘算法采用以下输入-– 从启用AI的CPS的操作中获得的时间序列轨迹，以及– 包含一般信息的文件，包括控制器频率、要求和设计文件。如果系统文档中没有提供，我们将使用此文档对启用AI的系统的初始HA进行• 它 采 用 相 对 无 约 束 最 小 二 乘 重 要 性 拟 合（RuLSIF）和基于密度的聚类算法的时间序列数据，以获得离散的模式转换的AI使能系统。• 它采用基于Fisher信息的分析和Cramer Rao界来推导每两个控制模式之间的保护和重置条件，如我们之前的工作（Lamrani，Banerjee和Gupta 2018）所执行的。• 对于每一个导出的模式，它采用多变量多项式回归 分 析 MultiPolyRegress 编 写 的 Ahmet Cecen 在MATLAB中央推导物理环境流量方程。• HA挖掘算法的输出是一个已学习的非线性混合自动机HALearned。• 然后，它评估新挖掘的HA（HALearned）与制造商提供的初始HA之间的一致性如果HA 学习与制造商提供的文件中定义的初始混合模型相同，则安全性结论无变化这种相似性表示为到达集比较，如图6所示。4.1RuLSIF变点检测方法变点检测技术的目标是发现隐藏在时间序列数据背后的突变。早期提出的变化检测方法对不同类型的变化不鲁棒最近在这一研究领域的努力引入了一种新的策略，该策略估计概率密度的比率，而不是直接估计密度（Liu et al.2013年b）。本文应用如 果 学 习 范 围设置安全，则系统安全安全保障1不安全的系统操作安全保障41-完全重叠或过近似不安全集达到2-欠近似或相交达到设定3-采矿系统相交了解到ReachSet SetLearnedMan已学习的范围集到达到达集合套网有学问的人到达集MAN不安全状态到达集MAN已学习到达集不安全状态到达集MAN已学习的范围集不安全状态不安全状态重叠面积小于误差界不安全状态重叠面积超过误差范围安全保障3安全保障2不确定的情况下，需要更多的数据来确定安全性不确定的情况，可能是由于采矿错误图3：安全性分析案例相对无约束最小二乘重要性拟合（RuLSIF）方法，据报告，该方法在稳健性、非参数收敛速率的最优性和数值稳定性的最优性方面优于竞争性方法（Aminikhanghahi和Cook 2017）。RuLSIF方法背后的主要思想是限制密度比，并使用α-相对皮尔逊（PE）散度作为相异性度量，其中0<α 1。因此，RuLSIF不相似性度量具有以下形式：PEα[p（ x ） ]||p′ （ x ） ]=P E （ p （ x ） ||αp （ x ） +（1−α）p′（x））。4.2多元非线性多项式回归分析我们考虑从一系列观测值中估计连续变量集合X之间的非线性关系的问题可以对多维数据执行多变量多项式回归例如，二元方程的二阶多项式具有以下形式：y=a1+a2xi+a3yi+a4x2+ a5xiyi+ a6y2，i = 1，.，n，其中n表示到达指定系统的集合，但它不与不安全集合相交。在这种情况下，我们可以保证系统在安全范围内运行。2) 挖掘系统的可达集是指定系统的可达集的下近似或与指定系统的可达集相交，挖掘系统不与不安全状态相交。这是一个不确定的情况，因为偏差可能是由于系统操作的变化，也可能是由于挖掘中的错误3) 已开采系统的可达集与不安全集相交，但相交面积在开采技术的误差范围内。这种情况也是不确定的情况，因为与不安全集合的交集可能是由于系统操作的问题或由于挖掘中的错误。4) 开采系统的可达集与不安全集相交，且相交面积大于开采技术的误差界在这种情况下，我们可以保证这是由于系统的不安全操作5评估在本节中，我们考虑提取人工胰腺（AP）控制的混合自动机我我数据点的数量。本文中，在将数据拟合到非线性多项式回归模型中以找到最佳拟合曲线的同时，对xi∈X关于时间的每个微分方程进行X中变量幂的回归（Ce- cen2017）。4.3安全保障我们假设制造商已经证明了系统的混合自动机表示的安全性。这意味着制造商提供的混合动力系统的可达集不会与不安全集相交，如图3所示。可达性分析的解决方案总是提供一个解决方案，这是一个过度近似的系统1995年）。关于学习系统，可以有四种不同的安全保证情况：1)学习系统的可达集是指定系统的过近似，系统本实验中使用的数据来自我们与MAYO诊所的合作。收集的数据包括CGM读数和膳食摄入量。为了获得剩余的不可访问信号，我们使用UVA/PadovaT1 d平台模拟1例T1 D受试者的间质胰岛素X和血浆胰岛素浓度I从I/O轨迹，我们应用我们的技术来获得学习的混合自动机，并将其操作与制造商提供的操作进行比较（Banerjee et al.2013年度）.我们比较推断和给定的混合自动机语义，找出两个模型之间的不一致之处。我们应用C2E2工具来执行我们的可达性分析评估（Fan et al.2016年）。人工胰腺（AP）：我们首先考虑AP控制系统的I/O轨迹。这里G和I是连续状态变量，也是控制器输入，外部胰岛素输注速率It是控制器输出。• HA挖掘算法的第一步是：✭✭−✭142完全重叠部分重叠（几乎完全）时间图4：RuLSIF I/O分段示例给定AP混合自动机模型的可达集AP推理混合自动机模型的可达集模式转换1模式转换2模式转换3我图6：学习HA和制造商提供的初始HA的到达集之间的比较。• 然后，HA挖掘技术使用Matlab中的多变量多项式回归MultiPolyRegress（在第4.2节中描述），使用I/O时间序列数据推断每个控制模式的流方程。对于血糖的变化，我们得到以下方程，其中轻微感染的患者可以排除癌症：✭✭✭˙✭✭✭−9✭✭−12✭✭−11G=π−4。6948X+1。1483I+1483−1483I。小行星7926G图5：模式转换的基于密度的聚类。如第4.1节所述，在I/O数据上使用RuLSIF发现I/O时序数据背后的突变，这些突变代表潜在的控制模式变化。从图4中，我们首先考虑模式集M={m1，m2，. . . m12} 12种不同的模式。• 对于人工胰腺，控制器决策与接下来30分钟内的连续状态变量的预测值在每个转换时间戳处，考虑模式转换之前和之后的控制器输出的值以及接下来30分钟内的连续状态变量的值。收集的时间序列数据用作基于密度的聚类算法中的特征，以将唯一的控制模式更改分组，如图5所示• 然后，HA挖掘技术为每个簇导出重置如果重置值不是驱动的恒定值，并且在集群中的每个数据点内变化，则我们采用Fisher信息和Cramer Rao界限来 推 导 It 与 G ， X 和 I 的 线 性 关 系 （ Lamrani ，Banerjee和Gupta 2018）。对于图5中用蓝色菱形描绘的从模式m2到m3It= 0。5 G +44。第七十五 章（四）-0。0316 84G−GX+−7。17 42−15GI+2。9149−201年。4819I.因此，HyMn为一个T1D受试者推断以下方程组：Gstec=−X（t）G（t）−0。03G（t）+2。第九条第五款Istec =-0。2 3I（t）−0. 09G（t）+17。03.（六）对于每个段，我们获得了具有不同重置条件It的相同方程组5和6，从而得出结论：m1、m2、m3是唯一模式，而不是复合模式（中断、基础和大剂量控制模式）。• 下一步是确定每个控制模式变化的保护条件在控制模式改变时，使用连续状态变量的观测矩阵，矩形或非矩形保护被学习为连续状态变量上的线性约束的结合，如我们以前的工作所报告的那样（Lamrani，Banerjee和Gupta 2018）。• 最后，在挖掘的HA和制造商提供的初始HA之间执行到达集比较，如图6所示。6讨论和结论这项工作的主要贡献是在启用AI的CPS的操作阶段进行安全验证的新方案。所提出的方法是基于混合自动机挖掘从操作的AI启用系统收集的痕迹。安全验证使用学习的混合自动机，并将其与制造商给出的系统规范进行比较，以确保系统的运行符合设计模式转换时间戳M7M8M9M10M11M12M1M2M3M4m5 m6rsonr安全性能。如果学习的混合自动机具有比制造商提供的参考规范模型更少的控制模式，则表示未命中模式的轨迹不存在于可用轨迹中由于I/O痕迹不足，学习的混合自动机将是参考规范模型的欠近似表示。在这种情况下，制造商应该提供完整的跟踪来完成挖掘过程。我们将所提出的技术应用于人工胰腺控制系统，并证明了这种安全验证技术的有效性所学习的HA和由制造商提供的初始HA的范围集之间的差异然而，使用学习的HA模型进行根本原因分析肯定是我们未来的努力之一我们确定了拟定安全性分析的所有可能结果，并确定了哪些病例可得出某些安全性结论，以及其他需要进行更多分析的病例。这可以为FAA或FDA等认证机构提供有关操作系统安全性的重要指令。所学习的HA的保真度基于数值保证，其包括通过计算两组迹线之间的均方根误差（RMSE）将收集的用于验证的I/O迹线（不同于训练中使用的数据）与使用推断的HA生成为所提议的方法制定正式的保证仍有待于今后的工作。另一个改进的方向是如何确定再次挖掘另一个自动机的合理时间段，以定期对启用人工智能的CPS进行安全验证。波音飞机的运行安全运行安全验证可用于了解波音飞机MCAS的运行情况。MCAS系统是一种自动俯仰控制系统，当飞机的迎角（AoA）非常高时，该系统被激活。当传感器的AoA读数高于制造商设定的阈值时，MCAS系统被激活。然后，该算法以每秒0.27度的速率将水平稳定器调整向上推至2.5度或最长9.26秒3。所提出的基于操作安全HA学习的技术可应用于学习表示两种控制模式MCAS启用和MCAS禁用的混合自动机、可使用表示每种控制模式中AoA变化率的微分方程表示的飞机环境模型以及能够从一种模式转换到另一种模式的防护条件这使波音公司的运营商能够了解MCAS的运作及其运作模式。如果MCAS的制造商允许访问其规范模型，则操作安全性允许在认证的MCAS操作与其在现实世界中的操作之间进行一致性验证3https://theaircurrent.com/aviation-safety/what-is-the-boeing-737-max-maneuvering-characteristics-augmentation-system-mcas-jt610/引用Abbas，H. Y. 2015. 网络物理系统的基于测试的伪造和一致性测试。博士美国亚利桑那州立大学博士论文。Besur，R.Courcoubetis，C.;Halbwachs，N.;Henzinger，T. 一 、 霍 ， P. - H. 的 ; Nicollin ， X.; Olivero ， A.;Sifakis，J.;和尤文，S. 1995.混杂系统的算法分析。Theoretical ComputerScience138（1）：3-34.Aminikhanghahi，S.，Cook，D. J. 2017.时间序列变点检测方法综述。知识和信息系统51（2）：339-367。安徒生，K. E、和Højbjerre，M. 2002. Bergman最小模型的一种近似方法胰岛素50（100）：200。Araujo，H.; Carvalho，G.; Mohaqeqi，M.; Mousavi，M.的R.;和Sampaio，A. 2018.网络物理系统的声音一致性测试：理论与实现。计算机程序设计科学162：35-54.Balakrishnan，H.; Hwang，I.; Jang，J.S.;和Tomlin，C.J. 2004.自治随机线性混杂系统的推理方法。混合系统国际研讨会：计算与控制，64斯普林格。Banerjee，A.;张玉; Jones，P.;和Gupta，S. 2013.采用正规 方 法 提 高 家 用 医 疗 器 械 安 全 性 。 BiomedicalInstrumentation and Technology47（SPRING）：43-48.Blackmore ， L.; Gil ， S.; Chung ， S.; 和 Williams ， B.2007.切换线性系统的模型学习。2007年第46届IEEE决策与控制会议，4648美国电气与电子工程师协会。Burmester，S.; Giese，H.;和Oberschelp，O. 2006.用于复杂自优化机电系统设计的混合uml组件。控制、自动化和机器人信息学。斯普林格。281-288.Cecen，A. 2017. 实际时空资料中空间统计之计算、利用与推论。博士毕业论文，佐治亚理工学院。Clarke ， W. L. 的 ; Anderson ， S.; 布 列 塔 尼 ， M 。 ;Patek，S.; Kash- mer，L.;和Kovatchev，B.2009年使用皮下葡萄糖传感和胰岛素输送以及模型预测控制算法的闭环人工Contag ， M.; Li ， G.; Pawlowski ， A.; Domke ， F.;Levchenko，K.; Holz，T.;和Savage，S.2017年。他们是如何做到的：现代汽车排放抑制装置的分析。2017年IEEE安全与隐私研讨会（SP），231-250. 美国电气与电子工程师协会。Dreossi，T.;弗里蒙特湾J.道：Ghosh，S.; Kim，E.;Ravan-bakhsh，H.; Vazquez-Chanlatte，M.;和Seshia，S.A. 2019年。Verifai：一个用于人工智能系统的形式化设计和分析的工具包计算机辅助验证国际会议，432斯普林格。范，C.;齐，B.; Mitra，S.; Viswanathan，M.;还有达吉拉拉P. S. 2016. c2e2非线性混合模型的自动可达性分析。计算机辅助验证国际会议，531-538。斯普林格。Frehse，G.; LeGuernic，C.; Donz e'，A.; Cotton，S.;Ra y，R.; Lebeltel，O.; Ripado，R.;Girard，A.;Dang，T.;和Maler，O.2011. Spaceex：混合系统的可扩展验证。计算机辅助验证国际会议，379-395。斯普林格。Lamrani，I.; Banerjee，A.;和Gupta，S. K. 2018.赞美诗：从网络物理系统的输入输出痕迹中挖掘线性混合 自 动 机 。 在 2018 年 IEEE 工 业 网 络 物 理 系 统（ICPS），264-269。美国电气与电子工程师协会。Leveson，N. 2011. 工程一个更安全的世界：系统思维应用于安全。MIT Press.刘，J.;刘志;他，J.; Mallet，F.;和丁、Z。2013年a.混合 marte statecharts 。 Frontiers of Computer Science7（1）：95-108.Liu， S.; Yamada， M.; Collier ，N.; 和Sugiyama， M.2013年b.用相对密度比估计检测时间序列数据中的变点。Neural Networks43：72-83.Ly，D. L.，和Lipson，H. 2012.学习混合动力系统的Journal of Machine Learning Research13 （ Dec ） ：3585-3618.Lyde，S.，也许，M。2013.从控制代码中提取混合自动机。在NASA正式方法研讨会，447-452。斯普林格。天哪，C。D.的; Micheletto，F.;吕，D.;布列塔尼，M。; Kovatchev，B.;和Cobelli，C. 2014. uva/padova 1型糖尿病模拟器：新功能。糖尿病科学与技术杂志8（1）：26-34。McDermid，J. A.;贾，Y.;和Habli，I. 2019.自主系统安全保障框架。在人工智能安全2019年，1CEUR研讨会论文集。Medhat ， R.; Ramesh ， S.; Bonakdarpour ， B.; 和Fischmeister，S. 2015.一个从输入/输出轨迹中挖掘混合自动机的框架。第12届嵌入式软件国际会议论文集，177Press.Minopoli ， S. ， 和 Frehse ， G. 2016. Sl2sx 转 换 器 ： 从simulink到spaceex模型。在第19届混合系统国际会议论文集：计算与控制，93-98。ACM。Niggemann，O.，和Lohweg，V.2015。关于信息物理生产系统的诊断：最新技术和研究议程。第29届AAAI人工智能会议论文集，4119-4126。Press.Niggemann，O.; Stein，B.; Vodencarevic，A.;迈尔，A.;和Buning，H. K. 2012年。混合时间系统的学习行为模型。见AAAI，第2卷，1083Niggemann ， O.; Windmann ， S.; Volgmann ， S.;Bunte，A.; Stein，B. 2014.使用学习模型进行网络物理生产系统的根本原因分析。InInt. 车间诊断原理（DX）.Russell，S.J.，和Norvig，P.2016年。人工智能：一种现代方法。马来西亚;培生教育有限公司。Santana，P.H.; Lane，S.; Timmons，E.;威廉斯湾，澳-地C.的; 和福斯特角2015.学习具有保护转换的混合模型。在AAAI，1847Schmitz，D.;张，M.; Rose，T.; Jarke，M.; Polzer，A.; J. J.H-czynski; Kowalewski，S.; Reke，M. 2009. 控制系统开发中需求模型到数学模型的映射.在欧洲模型驱动架构会议-基础和应用，253264.