混合系统安全性证明的数值辅助演绎方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记317（2015）19-25www.elsevier.com/locate/entcs动力总成控制系统的数值辅助演绎安全性证明我是Ar'echiga a，1，JamesKapinski b，Jyotirm oyV。Deshmukhb，还有普拉泽和布鲁斯·克罗a卡内基梅隆大学，5000 Forbes Ave Pittsburgh，PA，USAb丰田技术中心，1630 W。186th，Gardena，CA，美国摘要使用演绎技术，如定理证明器，在混合系统的安全验证中有几个优点。然而，在定理证明者在证明任务上取得进展所需的协助类型与系统设计者能够提供的协助类型之间往往存在差距。为了解决这一缺陷，我们提出了一个扩展的演绎验证框架的演绎动态逻辑，允许定理证明者KeYmaera本地原因的行为，通过利用外部方法提供的前向不变集，如数值技术和设计师的见解。 我们的主要贡献是一个新的推理规则，向前不变切割规则，引入到KeYmaera的证明演算。我们展示了切割规则的行动上的一个例子，涉及汽车动力系统控制系统，在其中我们利用模拟驱动的数值技术来计算一个本地的障碍函数。关键词：信息物理系统，混杂系统，验证，安全性1引言大多数网络物理系统本质上是混合的，即，具有由微分方程控制的连续状态演化和离散模式转变。不幸的是，验证混合系统的安全属性的问题是不可判定的[6]，并且用于验证软件的大多数技术并不直接适用。混合系统验证的许多方法都侧重于创建在固定时间范围内可达到的系统状态集的过度近似[9]，[3]，[4]，[2]。虽然这些方法享有高度的自动化，但它们在范围和可扩展性方面受到限制。另一种方法是采用演绎技术，尝试使用半交互式定理证明器构建安全性的符号证明[10]。与可达集计算技术不同，定理证明器可以处理非线性1这项工作部分由美国国家科学基金会资助，资助范围为NSF EXPEDITION CNS-0926181。http://dx.doi.org/10.1016/j.entcs.2015.10.0031571-0661/© 2015由Elsevier B. V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。20N. Aréchiga et al. /Electronic Notes in Theoretical Computer Science 317（2015）19⊆动力学直接，而不引入近似工件。此外，定理证明器可以处理涉及符号参数的证明任务通过定理证明对混合系统进行安全验证，可采用安全证书的形式，即，一个符号表达式，表示一个集合，包含来自给定初始集合的所有可达状态，同时排除不安全状态[1，10]。然而，设计人员通常对不同操作制度下的局部行为有更好的洞察力，而不是对整个系统的总体知识在[8]中，我们展示了一种发现局部不变量的数值技术该技术可用于搜索特定感兴趣区域中的局部不变量与以前专注于获得全球安全证书的工作相比，我们的方法鼓励本地推理和惰性构造此类证书。为了支持本地推理，我们引入了一个新的证明规则称为前向不变切割规则的定理证明KeYmaera演算。 这个规则类似于归纳不变量;给定一个操作区域和一个建议的局部安全证书（以前向不变量的形式），该规则允许我们将整个证明分解为三个证明义务：（1）证明建议证书的不变性，（2）证明局部证书保证安全，（3）证明除了与局部证书相关的区域相关的行为之外的我们证明了这一规则的案例研究的动力总成控制系统的安全验证。该系统是控制系统的简化模型，负责将汽油发动机中的空燃比（A/F）保持在最佳设定点附近。我们描述的整体证明，但主要描述的作用，向前不变的切割规则，以证明A/F比保持在10%的最佳设定点在KeYmaera。2混合系统和混合程序混合动力系统由一组连续值状态变量x和一个离散值状态变量q（也称为模式）组成，x从定义域XRn中取值，q从有限集合Q中取值。系统在连续或离散时间内演化，混合系统在时间t的配置可以通过其连续和离散状态变量的值来描述。在模式q中，连续值状态变量的演变通常使用形式为xstec（t） =fq （x（t））的普通微分方程（ODE）来描述，其中fq是从X到X的函数。虽然混合系统可以有外部输入，但在这里，我们只考虑自治系统，即，所有转换仅取决于系统状态的系统。允许系统从一个离散状态过渡到另一个（可能相同）离散状态的状态依赖条件称为保护。虽然混合自动机往往是一个方便的建模形式主义这样的系统，在这里，我们使用的混合程序符号，以方便使用的基- maera定理证明，我们的演绎方法的主力为了指定混合程序和规范，KeYmaera使用了由dL表示的离散动态逻辑2的形式主义。[2] dL的语法和语义在[10]中有详细描述;我们在这里只提供一个最小的概述N. Aréchiga et al. /Electronic Notes in Theoretical Computer Science 317（2015）1921LL→ ∧ ¬⊆→2.1逻辑dL一个混合程序是由语法指定的，α，β：：= x：= θ|x：= 0| {xJ1 = θ1，...，xJn = θn&H}|？H|α∪β|α; β|（ 1）其中，α，β是混合程序，θ，θ1，.， θn是项，H是逻辑公式。程序x：=θ意味着x被赋予项θ的值。程序x：=x意味着x被非确定性地赋予一个任意实数。程序{xJ1 =θ1，.，xJn = θn&H}意味着xi个变量在一段时间内连续变化，导数θi受到xi个变量所取的值在整个时间内满足H的约束。混合动力计划？如果逻辑公式H为真，则H表现为跳过，否则表现为中止其余部分遵循与正则表达式类似的符号，表示非确定性选择，;表示顺序组成，并且n表示任意重复。dL的公式由文法描述：φ，θ：= θ1= θ2|θ1≥ θ2|¬φ |φ ∧ ψ |φ ∨ ψ |φ → ψ |[α] φ|中国（2）其中φ，φ是d的公式，θ1，θ2是项，α是混合规划。 箱模态[α]φ意味着φ在混合程序α的所有迹之后保持，并且α3用前向不变割规则进行安全验证安全验证问题。 安全验证问题是决定混合程序α的状态是否总是包含在给定的安全集S内，当从指定的初始集I开始时（即，以决定I→[α<$]S）。如果一个集合包含初始集合，我们说它是初始化的，如果它不包含初始集合，我们说它是安全的。不安全集合，以及不变量，如果每当系统行为进入该集合时，该行为在所有未来时间都保持在该集合中。全局安全证书是一个初始化的、不变的和安全的集合。具有安全证书的参数使用不变证明规则在d中捕获，其中G是全局安全证书：I→G G→[α]GG→SI→[α<$]S（三）寻找全球安全证书的一般任务是困难的。在这项工作中，我们使用系统结构的知识来提出不变和安全的集合，但不一定要初始化，并在证明过程中利用它们。我们称这些集合为本地安全证书。前向不变切割规则。逻辑证明中的一个切口允许引入一个引理。我们引入了一个新的切割规则，根据我们的经验，通过利用局部不变性属性的知识来简化证明过程。下面的证明规则断言，如果一个集合CI是局部不变的（C[a]C）和安全（C）其余条件（I） C）可以单独解决，以证明 安全为代价的我们注意到，我们可以证明这个证明规则是合理的，但为了简洁起见，省略了证明。22N. Aréchiga et al. /Electronic Notes in Theoretical Computer Science 317（2015）19规则3.1（前向不变切割规则）IC→ [（α;？<$C）<$] S C → [α] CC→SI→ [α <$] S（四）我们注意到（3）中的第一个分支涉及一个全局不变集G，它必须对所有初始状态I成立，但前向不变割集C不必对所有初始状态I成立。因此，（4）中的第一个分支对应于I中不包括在C中的状态。获得前向不变量的数值方法 本文简要介绍了一些现有的生成安全前向不变集的技术。在混合系统社区中，屏障证明已经被提出作为一种类似于Lyapunov的分析技术，以证明从初始状态集合X0开始，没有系统轨迹进入不安全集合U[11]。为了发现屏障证书，我们采用了[12]中技术的修改，该技术使用具体的系统执行来生成一系列候选屏障函数。我们的技术基于[8]，使用具体的执行来生成一组线性约束。线性约束用于构造候选序列。最终候选者使用能够处理实数上的非线性理论dReal的满意度模理论（SMT）求解器进行验证[5]。4发动机燃油控制案例研究模型 我们提出了一个案例研究，涉及一个混合动力系统代表的汽车燃油控制系统。环境问题和政府立法要求燃料经济性最大化，废气排放最小化。在理想的空燃比（A/F），也被称为化学计量比，这两个量都是优化的。我们研究的汽车控制系统，其目的是准确地调节A/F比。系统动力学和参数来自已发表的模型[7]，然后简化，如[8]所示。该模型包括负责进气和空燃比测量的发动机子系统控制器的目标是将空燃比保持在标称运行条件的10%以内。我们模拟的实验涉及以固定速度运行的发动机控制器具有两种操作模式：（1）恢复模式，其以开环方式控制燃料，即，仅具有前馈控制作用，其中系统运行最多8 ms，以及（2）正常运行模式，其使用反馈控制来调节A/F比。控制器测量通过进气歧管的空气流量（用于估计歧管中的空气压力）和空气中的氧含量。废气，它用来计算空燃比。恢复模式表示当从传感器故障恢复时控制器的行为（例如，引起传感器读数可疑的异常传感器读数或环境条件）。在恢复模式期间，控制器不能访问氧传感器测量结果，并且必须以前馈方式操作（即，仅使用歧管空气流速）。正常模式是典型的操作模式N. Aréchiga et al. /Electronic Notes in Theoretical Computer Science 317（2015）1923.Σǁ ǁ{1} |≤ }→算法1：闭环燃料控制系统的d-L模型1EF CI→[m1m2s1→2s{1，2}→failmfail]S2I（（τ=0）（M=回收率）（pest=0）（i=0）（−10−3≤p≤10−3）<$（−10−3≤r≤10−3））3m 1 m（？M=回收率;？τ≤ 0。008;{1. 2. 3. （-0。86≤l1≤0。74）（−0. 17≤l2≤0. 18）（−0. 81≤l3≤0. 第六十八章）<$（p′= l1）<$（r′= l2）<$（p′est = l3）<$（i′= 0）<$（τ′= 1）&τ≤ 0. 008}）4s 1 ›→2s（？M=recoverry;？τ≥0。008;M：=正常;）5m 2 m（？M=正常;{（p′= fp）<$（r′= fr）<$（p′est = fpest）<$（i′= fi）&（−0. 02 ≤p≤0。02）（−0. 02≤r≤0。02）（-0。02 ≤pest≤ 0。02）（−0. 02 ≤i≤ 0。02）}）6 s{1，2}›→fail（怎么样？r<−0。1μ r> 0。1个;M：=fail;）7mfail？r<−0。1 μr > 0。1;M：=未通过）8SM/=未通过其中氧传感器测量值用于反馈控制。算法1是表示该系统3的混合程序。表示各模态连续动力学的常微分方程和模型参数被简略地省略了，但它们可以在[8]中找到。状态变量p_i、r_i、p_es_t和d_i表示歧管压力、实际空燃比与空燃比值之间的比率、歧管压力的控制器估计值以及PI控制器的内部状态;这些变量都已被转换，使得平衡点与原点重合。在恢复模式中，连续时间状态x是元组（p，r，pes t，ri，τ）。报告中的数据状态变量表示根据ODEτstec=1进行赋值的定时器的状态。在正常模式中，状态是gi venbyy（p，r，pes t，pi）。 我们假设系统在1. 恢复模式初始化时标称值的0%。这表示系统先前处于将A/F比精确调节到所需设定点的操作模式的情况。 目的结构域 对于状态变量，由x∞<0给出。2，其中包含状态变量的合理值的集合。使用前向不变割的安全性证明。验证目标是确保在给定的实验设置中，系统在固定恢复时间8后始终保持在标称A/F比的10%以内。0 ms已过去。我们描述了一个交互式的证明使用KeYmaera。为了帮助证明过程，我们使用第2节中概述的数值技术生成了一个障碍函数B：RnR。3 .第三章。然后，我们使用由障碍包围的集合xB（x）0来公式化前向不变割：C_∞（M =正态）_∞（B（x）≤ 0）。（五）我们应用前向不变切割推理规则（4），产生了KeYmaera必须履行的三个证明义务。义务1：C → [α] C。 从C语言的定义出发，给出了混合程序m1和[3]注意，混合程序中出现了明显的冗余，这是由于将系统表示为混合自动机到混合程序的显式转换。24N. Aréchiga et al. /Electronic Notes in Theoretical Computer Science 317（2015）19阿克斯→s1 →2可以忽略，因为两者都有混合程序？M=回收率作为第一项，这与C不一致。因此，这个义务只需要证明程序m2，s{1， 2} →fail，和mfail。为了履行程序m2的这一义务，我们使用我们添加到KeYmaera证明演算中的屏障证明规则I→（B（x）≤0）（B（x）= 0）→Δ B·f（x）0（B（x）≤0）→S<阿克斯I→[{xJ=f（x）}]S（六）为了应用屏障证明规则，我们使用算法1中定义的初始状态I，并将S替换为C。障碍证明规则中的第一个和第三个证明义务由于我们对障碍函数的选择和前向不变切割的性质而得到了微不足道的满足对于中间证明义务，KeYmaera询问dReal查询（B（x）= 0）<$（<$B·fnormal（x）>−<$）是否不可满足。为了解除m2，s{1， 2}›→fail的证明义务，KeYmaera需要证明如果B（x）0成立，这些程序中的任何一个都不能通过转换到模式fail来使C无效。< 它通过证明集合B（x）0是<使用dReal安全设置。义务2：C S。 这个义务是微不足道的，因为S要求模式除了失败之外什么都行，而C说模式是正常模式。义务3：IC→ [（α;？[C] S. 在这里我们引入C1，它对IC中的所有初始条件都是不变的。C 1（M/=失败）（0 ≤τ≤ 0. 008）X（x∈Sreach）（7）这里Sreach是通过使用dReal计算的p stec和r stec上的上界和下界对可达集的过近似。这里有一个明确的障碍证明应用程序，表明正常模式，当在这个集合中开始时，落在障碍证明内，因此也尊重这个不变量。这需要一个派生的否定性参数，KeYmaera通过查询dReal解决了这个问题。其余的由KeYmaera的标准演绎程序处理结论我们演示了如何利用动力系统控制系统的本地知识来提出一个不变和安全的集合。我们使用该集合应用前向不变割规则来证明系统的安全性引用[1] BernhardBe ckert ，ReinerHahnle，andPeterH Schmitt. 面向对 象 软 件 的 验证：关键方法 。Springer-Verlag，2007.[2] Xin Chen，Erika Abraham，and Sriram Sankaranarayanan. Flow*：An Analyzer for Non-Linear HybridSystems.在CAV，2013年。[3] Goran Frehse PHAVer：对HyTech之后的混合动力系统进行验证。STTT，10（3）：263-279，2008.[4] 戈兰·F·塞尔斯、科拉斯·勒·格尔尼克、亚历山大·唐·泽、斯科特·科顿、R ajarshiR ay、奥利维尔·勒·贝尔特尔、鲁道夫·里帕多、安托万·吉拉德、陶·当和奥德·马勒。SpaceEx：混合系统的可扩展验证。在CAV，第379-395页[5] Sicun Gao，Jeremy Avigad，and Edmund M Clarke.δ-完全可满足决策程序在真实的。 在j. 自动推理，第286-300页，2012年。[6] Thomas A. Henzinger，Peter W. Kopke，Anuj Puri，and Pravin Varaiya.混合自动机的可决定性是什么. JCSS，57（1）：94[7] Jyotirmoy V. Deshmukh，James Kapinski，Koichi Ueda，and Ken Butts. 动力系统控制验证基准。在混合系统：计算和控制，2014年。N. Aréchiga et al. /Electronic Notes in Theoretical Computer Science 317（2015）1925[8] 詹姆斯·卡平斯基，我的儿子。 Desh mukh，SriramSan k aranar ayanan，andNi k os A r'echiga. 混合动力系统的仿真引导的lyapunov分析。在混合系统：计算和控制，2014年。[9] 詹姆斯·卡平斯基和布鲁斯·H·克罗。具有扰动输入的离散时间滑模系统的渐近界ACC，第2852-2857页，2004年[10] 我是普拉泽。混杂系统的逻辑分析。Springer，2010.[11] 史蒂芬般若。非线性和混合系统验证的优化方法。博士论文，加州理工学院，加州理工学院，帕萨迪纳，加利福尼亚州，美国，2005年。[12] 联合Topcu，P. Seiler，and A.帕卡德利用模拟与平方和规划进行局部稳定性分析。Automatica，44：2669