使用MathSAT解决混合系统有界可达性问题

理论计算机科学电子札记119（2005）17-32www.elsevier.com/locate/entcs使用MathSAT1的工业混合系统Gilles Audemarda，Marco Bozzanob，Alessandro Cimattib和Roberto Riztianic，2a透镜信息研究中心IUTdeLens，Ruedlaudemard@iut-lens.univ-artois.frbITC-IRST，Via Sommarive 18，38050 Povo，Trento，Italy{bozzano，cimatti}@ itc.itcDIT，Universita`diTrento，ViaSommarive14，38050Povo，Trento，Italyrseba@dit.unitn.it摘要实际相关的工业系统通常可以用离散控制变量和实值物理变量来表征，因此可以建模为混合自动机。不幸的是，随着时间的推移，或三角形约束的物理行为的连续性，往往必须假设，这产生了一类不可判定的混合自动机。本文提出了一种线性混合自动机有界可达性的判定方法，该方法是基于将有界可达性问题归结为MATHSAT问题，即满足性 命题变量和数学约束的布尔组合。MathSAT求解器可用于检查有界长度的路径是否存在该方法在精神上与基于SAT的有界模型检查非常相似;此外，直接推理实变量的能力使计算杠杆超过基于离散化的方法。尽管一般问题的不可判定性，所提出的方法是能够提供有价值的信息，实际相关的大型设计关键词：形式验证，混合系统，SAT1这项工作已赞助的计算！国际水文计划RTN欧洲委员会项目（合同号：HPRN-CT-2000-00102），因此受益于委员会通过国际水文计划提供的财政捐助。它也得到了欧洲赞助的项目ESACS的部分支持，合同号为2010年12月28日。G4 RD-CT-2000-00361，并由英特尔公司授权2由MIUR COFIN 02项目赞助，代码2002097822 003。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.12.02218G. Audemard等人/理论计算机科学电子笔记119（2005）171介绍许多与工业相关的系统和工厂（例如，发动机，涡轮机）根据离散控制变量和物理实值变量（例如，速度、压力），并且可以自然地建模为混合自动机：取决于离散状态（例如，“标称”，“增加”），不同的方程描述物理变量的行为（例如，speed）。通常，物理变量的动态是连续的：即，从一个离散状态到另一个离散状态的转变不一定会在物理尺寸上产生不连续性。例如，在从“增加”到“减少”的过渡中此外，演化可以取决于物理变量值之间的比较。不幸的是，无论是强制连续性还是允许变量之间的比较（也称为三角约束）都会导致一类混合自动机，其中甚至可达性都是不可判定的[12]。然而，能够开发允许正式验证这种设计的工具是非常重要的，这些设计通常实现关键功能（例如，航空电子设备的控制系统）。在本文中，我们解决的问题，验证具有连续变量和三角形约束的混合自动机。我们提出了一个形式化的有界可达性验证方法。该方法基于将有界可达性问题编码为MATHSAT问题，即检查命题变量和实变量上的数学约束的布尔组合的满足性的问题。该方法通过使用有效的MathSAT求解器[1]变得实用，该求解器扩展并集成了最先进的命题满足性（SAT）技术和一组数学推理机。本文提出的方法在很大程度上类似于有界模型检查[4]，并增强了[3]中提出的方法，仅限于时间系统，以处理具有任意线性动态的实变量。所提出的技术显然是不完整的，目前仅限于线性动力学的情况下。尽管有这些事实，但是，它允许我们表示和分析来自现实世界应用的有趣系统[6，5]，提供有用的信息，特别是面向调试和目标导向的仿真。实验分析表明，我们的技术是有竞争力的最先进的验证工具，如HY TECH，并与基于实变量的离散化的方法。G. Audemard等人/理论计算机科学电子笔记119（2005）1719我阀我ATSMGBXATSMPTOGBX计算机计算机PTOUTILATSM：空气涡轮启动电机GBX：齿轮箱我：主机PTO：动力输出轴UTIL：公用事业文件概要Fig. 1. SPS示意图本文其余部分的结构如下。 在第2节中，我们举例说明一个激励我们的方法的例子;在第3节中，我们给出了一个简短的和非正式的介绍我们的混合系统模型;在第4节中，我们给出了一个简短的概述基于SAT的有界模型检查，我们更详细地讨论了我们的混合系统编码到MATH SAT;在第5节中，我们讨论了一些实验，最后在第6节和第7节中，我们讨论了相关的工作，并得出一些结论。2一个鼓舞人心的例子：二次电源系统在整个文件中，我们使用一个运行的例子来激励和说明我们提出的主要概念具体来说，我们讨论了一个现实世界的安全关键系统，即二次电源系统（SPS）的建模和分析这是一个工业案例研究，已经并正在ESACS（复杂系统增强安全分析）中进行研究，ESACS是欧盟赞助的航空电子领域项目，其目标是定义一种方法来改进复杂系统开发的安全分析实践[6，5]。SPS驱动飞机的液压和电气设施。它是一个具有嵌入式硬件和软件组件的安全关键系统的例子。硬件子系统包括（电）机械部件（例如，控制阀、继电器、轴、齿轮箱、飞轮）和电子传感器（例如，速度和压力传感器），而软件组件是由嵌入式控制器（SPS计算机）提供。UTIL20G. Audemard等人/理论计算机科学电子笔记119（2005）17、、、没有失败sp me≥sm1sp me≤sm2J、、、握柄spsp me-k1（英语：sp me-k 1）spme≥sm4sp me≤sm2 J、、、速度sm4sp me=sm4J\\ \ ，\\命名spsp me-k2（双头）spme≥sm3sp me≤sm2速度sm3sp me=sm3JJ图二. SPS：主机自动机（ME）SPS驱动飞机左侧和右侧的公用设施。为了确保基本安全要求，即没有单一故障会导致SPS公用设施的全部损失，系统的架构包括两个基本冗余：存在两个独立且完全对称的管线，其目的是分别驱动左手侧和右手侧设施;对于每一侧，在机械管线中的一个部件失效的情况下，相关设施的机械驱动（正常模式）由气动驱动（交叉泄放模式）来补充。图1显示了SPS的简化示意图。SPS的正常运行包括将机械动力从发动机传输到相关的液压发电机和发电机。特别是，主发动机（ME）的机械动力通过动力输出轴（PTO）传输到齿轮箱（GBX），为公用事业提供动力。组件可能由于异常操作条件或破裂而失效。作为一个例子，主机的两种可能的故障模式是掉油和抓地为了确保夜间操作的安全性，在发动机故障的情况下，SPS计算机自动启动交叉放气程序，该交叉放气程序包括通过空气涡轮马达（ATSM）使用来自阀（EGR）的放气来驱动交叉放气程序的正确运行是SPS的一个安全要求的示例关于这一点的一些实验结果将在第5节中给出。3混合自动机建模在这一节中，我们简要介绍了混杂系统的模型和构造方法。该模型受到[10，11]中提出的线性和矩形混合自动机模型的启发 非正式地说，混合系统可以被看作是sp me=sm4sp me=sm3\G. Audemard等人/理论计算机科学电子笔记119（2005）1721、、、打开很近？、、、关闭p阀≥p1p阀≤p2J开着吗p阀=0J、、卡在打开卡在关闭p阀≥p1p阀≤p2p阀=0JJ图三. SPS：阀门自动机（VELCADE）混合自动机集合的组成，它们可以通过在某些通道上显式同步或通过共享变量隐式地进行通信。每个自动机对离散事件（例如，组件的故障时间、分量速度）。在任何给定的时刻，混合自动机的状态由控制位置（离散状态）和所有模拟变量的值（连续状态）定义。状态可以由于瞬时离散转变而改变，这改变了控制位置并且还可以改变模拟变量的值（例如，重新初始化是可能的），或者是因为时间流逝（连续）转换，这只会根据某些特定的规律改变模拟变量混合系统可以被看作是[3]的定时系统模型的扩展，其中唯一的模拟变量是时钟。在下文中，通过初等线性表达式，我们意指线性项上的等式和/或（非严格）不等式（即，实值变量与有理系数的线性组合）。图2和图3描绘了混合自动机的两个示例，对SPS的主发动机混合自动机由以下组件组成位置一组有限的位置，对混合自动机的离散状态进行编码。图2中的自动机有五个位置，画成圆圈，模拟SPS的ME的离散状态。位置无故障模型发动机的默认行为;位置抓地力和熄火模型两种不同的故障状态;位置速度sm4和速度sm3模型状态，其中发动机速度具有恒定值sm4和sm3。模拟变量实值数据变量的有限向量（w1，...，w n）。图2中的spme变量对ME的速度进行时钟变量[3]中的可以看作是实值变量的一种特殊情况底漆22G. Audemard等人/理论计算机科学电子笔记119（2005）17}--变量（例如，sp_me_J）用于表示执行转换之后的实值变量的值。初始和不变条件混合自动机的每个位置都可以被声明为初始（意味着它是系统的合法初始状态）。每一个位置都可以配备有关于实值变量的不变量，这些不变量由一组初等线性表达式表示{101，.，拉克什在变量w1，...，w n. 位置无故障是初始ME自动机的位置（图2），并配备了一个不变的，ant强制执行sp me变量之间的常数值sm1和sm2。位置速度sm3的不变量迫使sp me不断地假设值sm3。通道一组有限的通道用于自动机之间的离散通信通道c可以用作输入（符号c？）或输出（符号c！）用于同步不同自动机的通道。例如，图3的压力阀自动机使用两个不同的输入通道，称为open？关闭？预期的语义是压力阀自动机等待来自相关SPS计算机控制器的传入命令（请求打开或关闭阀）转换一组有限的离散转换对自动机的离散每个转变（也称为开关）具有源和目标位置，并且可以配备有集合{γ1，.，γ k}个防护装置（先决条件）和一组θ1，.，跳跃条件的θ m（后置条件）在实值变量上。一个守卫是一个关于w1，...，一个跳跃条件是一个初等线性表达式在w1， . ，wn，w1J， . ，wnJ. 在图2中，从flameut到speedsm3的转换具有保护SP_ME=SM3并且没有跳转条件。 按照惯例，在转换上不存在跳转条件迫使实值变量保持它们的值（例如，在前面的例子中，SP_ME_J=SP_ME隐含地成立）。转换可以配备一个或多个可选标签，表示自动机必须同步的通道。例如，图3中的两个转换标记为输入通道打开？和关闭？变量动态变量动态描述了实值变量如何在存在时间流逝转变的情况下改变，并且对于每个位置被表示为集合{R1，...，上的初等线性表达式w1， . . . ，wn，w1J， . 作为示例，在图2中，位置抓地力中的spm变量k1是常数），也就是说，速度线性下降（与时间延迟成比例），一阶导数等于k1。表示时延的表达式将在4.2节中解释。G. Audemard等人/理论计算机科学电子笔记119（2005）1723¬¬¬i=0时i=0时i=0时这里提出的混合自动机不属于[10]中描述的矩形自动机因此，甚至这类自动机的可达性问题也是不可判定的[12]。4混合系统的有界模型检测在本节中，我们给出了一个非常简短的概述SAT基于模型检查，我们讨论了我们的混合系统模型的编码，非正式地描述在第3节，到MATH SAT。4.1基于SAT的有界模型检测Bounded Model Checking（BMC）是符号模型检验的一种新方法[4]。 给定Kripke结构M和LTL公式f，是通过寻找反例来检查f在M中是否为真（即，可以在k步的范围内呈现的违反f）的见证。给定k，问题被简化为命题公式[[M，<$f]]k.例如，对于形式为f：=Gp（s）的属性，其中p（s）是布尔变量s中的布尔公式，则k k−1k[[M，<$f]]k=I（s（0））<$C（s（i））<$R（s（i），s（i+1））<$p（s（i）），其中I（s（0））是初始条件的表示，C（s（i））是步骤i处的不同条件的表示，并且R（s（i），s（i+1））是从步骤i到步骤i+1的过渡关系的表示如果[[M，<$f]]k是可满足的，命题模型提供了一个到f的k步的反例。 如果[[M，f]] k是不可满足的，那么M的反例的存在就无从谈起了。|f的最高边界。典型的技术是生成并求解[[M，f]]k，以增加k的值，直到找到反例或达到给定的超时BMC作为一种实用的技术越来越被接受，特别是在伪造过程中，即bugfinding.该技术依赖于使用高效的SAT求解器（例如，基于DPLL程序[8]），用于检查[[M，f]] k的命题满足性。 如[7]所示，BMC避免了基于二叉决策图的模型检查可能发生的内存爆炸，因此能够处理更大的电路。24G. Audemard等人/理论计算机科学电子笔记119（2005）17努尔4.2编码我们对混合自动机的验证方法是BMC对时间系统的推广，如[3]中所提出的。该方法将定时系统的BMC问题简化为决定数学公式的满足性的问题，即布尔变量和实数变量上的线性（非）等式的布尔组合，表示绝对时间和时钟。由此产生的数学公式处理与M ATH SAT [2，1]，一个求解器结合了一个高效的DPLL程序与数学约束求解器，增加演绎能力。在时间自动机的编码中，布尔变量用于对系统的离散部分进行编码，而实变量的线性约束用于对时间部分进行编码。特别地，每个位置l由逐位编码l表示，使得当且仅当系统处于位置li时li成立;每个同步事件（通道，共享变量）由相应的布尔变量表示;每个开关由单个布尔变量（比如T）表示，当且仅当系统执行相应的开关时，该布尔变量保持;表示连续转换的布尔变量Tδ，当且仅当时间流逝某个δ >0时，该布尔变量保持;最后，对于每个进程Pi，我们引入导出一个布尔变量T i，当且仅当进程P i不做任何事情时它才成立。为了处理时间，我们引入一个表示绝对时间的实值变量t，并且对于每个时钟x，引入一个表示相对于绝对时间的偏差的实值变量ox。编码中所需的所有数学约束的形式为v1−v2da c，da∈ {≤，≥，=，>，<}v1V2是表示绝对时间或时钟值的实变量读者可以参考[3]了解详细信息。我们处理的情况下，混合自动机考虑，这是一个扩展的情况下，时间自动机。通过引入一组表示物理实体的实变量ωi，为了简化符号，在下面我们写：我们写“c ·t. “代表“c · t j − c · t. ”;“ω≤... “f or“ω j ≤ ω +. “.我们还将“（w ∈ [t1，t2]）”表示为“（w ≥ t1）<$（w ≤ t2）"，其中t1和t2是线性项。 如果是一个公式，则J表示在中将每个命题变量p j代入pJj，将每个实变量vi代入viJ得到的公式。4.2.1初始条件I（s（0））。在步骤0，在初始位置l中，ω可以是：G. Audemard等人/理论计算机科学电子笔记119（2005）1725----努尔--−∞−∞• 被设置为给定的初始值C0。如果是这样，我们用公理来表示这个事实l（0）→（ω（0）=c0）;（1）• b∈ [ −∞，∞ ]，a 0，b 0 ∈ [a0，b0]，b0∈[a 0，b 0 3如果是这样的话，我们用下面的公式来表示这一事实：l（0）→（ω（0）∈[a0，b0]）.（二）4.2.2不变条件C（s）。对于每个配备有集合1，...，关于实值变量的不变量的公理，我们包括公理l→α j。（三）J4.2.3转移关系R（s，SJ）。对于配备有集合{γ1，.，γ k}的保护，并且具有集合θ1，.，本文讨论了实值变量ω i s和t上的跳跃条件θ m ， 并 给 出 了 如 下 公理T→γj，（4）JT→θjJJ（五）分别对于每个物理变量ω，它不受开关T的跳跃条件的影响，因此必须保持其值，我们添加公理：T→（ω = 0）。（六）当进程i什么都不做时，对应于Ti，每个物理变量ω保持其值：伊努勒 →（ω = 0）。（七）当时间在位置l中流逝时，物理变量ω i根据变量动态集合ω 1，…，与L. 对于每个位置，我们添加公理（1Tδ）→ δi （8）我可变动态的不同形式是可能的：3 “a 0 =“a n d“b 0 =“意味着没有低的库存，也没有高的库存。ω分别。不26G. Audemard等人/理论计算机科学电子笔记119（2005）17--• ω在以下形式的动态下保持其值：（1Tδ）→（1ω = 0）;（9）• ω可以根据线性函数确定性地演变：（lTδ）→（ωω =c· ωt）（10）c是一个常数。• ω可以在两个线性函数内非确定性地演变：ωJ∈[b1ω+c1·t−a1，b2ω+c2·t+a2]，（11）a1，a2≥0，b1，b2∈{0，1}，c1，c2∈（− ∞，∞）.（十二）如果a1=a2=0，则n（11）表示一个三角约束.如果b1=b2= 0且c1= c2= 0，则（11）对矩形约束进行编码。• 在一般情况下，变量的演化在由线性不等式1，...，如等式8所示。属性的编码基本上遵循[3]中的编码。我们的方法是有界完备的，在以下意义上：如果存在一个长度为k的迹，那么长度为k的编码是满意的，并且可以通过在其上运行MATHSAT来找到。 我们正在处理的问题告诉我们，一般来说，不可能确定是否可以找到一个具有更大k的反例，或者问题是否不可解。5实验评价我们评估的潜力的方法，通过解决一个例子的混合系统的工业相关性，即模型的 SPS 。 第 4 节 中 描 述 的 有 界 可达 性 方 法 既 可 用 于 模 型 调 试 （ 即 ，bughunting）和用于混合系统的仿真。在下文中，我们通过展示一些实验结果来提供有关使用我们的方法的一些提示为了便于说明，我们将讨论SPS案例研究的简化单侧模型，包括图1中ME、GBX、ATSM、PTO和SPS计算机组件的一个实例。在这种抽象下，系统的相对侧的类似组件被假设为正确工作。要检查的属性的示例由以下公式（的否定）（！GBX loc坏&了！GBX 抓住了&！阀. 锁定卡在关闭位置&！ATSM。loc坏了！动力输出轴loc fused）UGBX sp gbx<= sg1（P1）这是通过LTLuntil运算符表示的典型安全属性。 预期的语义是是否存在路径，使得G. Audemard等人/理论计算机科学电子笔记119（2005）1727时间T0：位置：无故障，gbx pto驱动，atsm空闲，sps正常，关闭模拟变量：sp me=sm2，sp gbx=sg2，sp atsm= 0离散传输：megrippage同步：无时间T1：位置：grippage，gbx pto driven，atsm idle，sps ok，closed模拟变量：sp me=sm5，sp gbx=sg3，sp atsm= 0离散变速器：atsm inc a，sps inc a，valve open同步：SPS和ATSM开启，SPS和ATSM开启时间T2：位置：grippage、gbx pto driven、atsm inc a、sps inc a、打开模拟变量：sp me=sm6、sp gbx=sg4、sp atsm=sa2离散传输：atsm inc ainc b、sps inc a inc b同步：SPS和ATSM oninc b时间T3：地点：grippage，gbx pto驱动，atsm公司b，sps公司b，开放模拟变量：sp me=sm7，sp gbx=sg1，sp atsm=sa3见图4。 一个MathSAT跟踪GBX、ATSM和PTO分量沿着路径发生，并且最终齿轮箱的速度（GBX分量）下降到恒定值sg1以下。上述属性的否定可以被视为要由系统验证的安全属性（即，在仅由于主发动机而出现故障的情况下，变速箱速度不能下降到SG1以下）。这一特性背后的基本原理是，由SPS计算机（见第2节）启动的交叉引气根据为常数sg1选择的值，该属性可能成立，也可能不成立。特别是，如果为sg1选择的值超过给定阈值，则MathSAT会伪造该属性（这意味着交叉放气程序无法防止齿轮箱速度降至该标准以下ticular值）。在这种情况下，MathSAT生成一个输出跟踪，显示导致违规的系统执行。该跟踪包括关于自动机所采取的离散转换和时间流逝转换的如果常数sg1的值被选择为低于合适的阈值，则特性（P1）因此，MathSAT没有找到任何反例。关于常数sg1的选择，见第7节的讨论.MathSAT生成的轨迹如图4所示。对于每个时刻，迹线示出ME、GBX、ATSM、和自动机的当前位置，spme、spgbx、28G. Audemard等人/理论计算机科学电子笔记119（2005）17- ≤≥、、、、、、、、、sps oksp gbx≥sg2sps inc a sps inc bsp gbx-sp atsm≥c1JJJ图五. SPS计算机自动机（片段）SPATSM模拟变量、在该时刻发生的离散转换为了更好地理解轨迹，在图5中，我们展示了SPS计算机自动机的简化版本（仅显示了与模拟相关的部分请注意，此自动机显示为三角形约束的示例，即sp gbxSPATSMc1[c1]，以及与共享变量（变量SPgbx和SPatsm）的通信型号，分别为GBX和ATSM组件的速度该模拟在时间T0开始，此时发生发动机抓地力。发动机和变速箱的速度都开始降低。在时间T1，SPS计算机检测到齿轮箱低速状态，因此发出阀门打开（SPS和SPS计算机自动机在开放通道上同步）;因此，ATSM开始增加其速度（SPS和ATSM在inc a通道上同步）。在时间T2，SPS计算机发出ATSM动态的改变（SPS和ATSM在inc b上同步）。当变速箱速度达到值sg1时，模拟在时间T3处停止。同样的方法也可以用于引导模拟。举个例子，我们考虑以下公式：（！我我loceng flameout&！GBXloc坏&了！GBX锁定夹持&！阀. 锁定卡关闭&！ATSM。loc坏&了！动力输出轴loc fused）UGBX sp atsm>=sa1（P2）它是先前可达性属性的变化，这里我们要求在路径的末端，ATSM组件的速度大于常数值sa1。此外，通过明确排除发动机故障，我们将主发动机可能的故障模式限制为抓地力。如第2节所述，在发动机出现故障的情况下，ATSM部件负责执行交叉放气程序，该程序包括利用来自阀门的气动动力驱动变速箱。交叉放气程序的正确运行需要ATSM（初始怠速）启动并提高变速箱速度。使用MathSAT，我们可以 以重建对应于上述属性的迹线，其示出了如何执行交叉出血过程。可以调整上述模拟，并通过在要查找的跟踪上添加更多约束来执行更多模拟sp gbx - sp atsm≤c1incb！sp gbx≤sg2inca！打开！G. Audemard等人/理论计算机科学电子笔记119（2005）1729物业P1物业P2K 时间时间Mem.结果时间时间 Mem.结果20.060.065.6UNSAT0.100.105.5UNSAT30.200.266.2UNSAT0.160.266.0UNSAT40.530.797.1UNSAT0.300.566.8UNSAT51.812.607.7UNSAT0.491.057.5UNSAT66.499.098.4UNSAT0.841.898.2UNSAT74.5313.628.9坐1.533.428.8UNSAT82.886.309.4UNSAT94.9411.2410.0UNSAT108.6919.9310.7UNSAT118.8828.8111.3坐表1实验结果（时间以秒为单位，内存以MB为单位）我们的方法对上述实施例的性能报告在表1中。对于每个问题长度，我们显示了计算时间，该问题实例的总计算时间和内存使用情况。计算时间包括分析和搜索时间。结果已经获得了奔腾III机1.0 GHz，256 Mb内存，运行LinuxRedhat 7.1。 MathSat为P1生成的最小长度轨迹长度为7，而为P2生成的长度为11。我们还尝试与HY TECH[11]进行比较，H y T ech是一种用于分析混合系统的最先进工具。 与我们的方法不同，H YTECH基于可达状态空间的计算，因此不限于有界情况。原则上，HY TECH在处理一类不可判定的自动机时可能不会终止（如SPS的情况我们编码的SPS模型，尽可能接近，到HY TECH。在底层多面体库中的错误太多，使得HYTECH不可能计算超过第5次迭代的可达构形的空间。我们还尝试使用-o 1和-o2选项，这有时能够限制此类问题，但在我们的情况下没有获得任何效果。从性能的角度来看，HYTECH在没有选项的情况下运行时达到第5次迭代所需的时间为32秒;使用-o 1和-o2分别需要50秒和86秒分析是非常初步的，但似乎表明我们的技术有明显的潜力6相关工作本文中提出的工作建立在我们以前对定时系统的工作基础上[3]。在[3]中，我们展示了如何将定时系统的有界模型检查问题简化为数学公式的可满足性，该数学公式可以30G. Audemard等人/理论计算机科学电子笔记119（2005）17然后由SAT解算器进行检查。我们还介绍了MathSat求解器[2，1]，这是一种有效的SAT求解器，它基于SAT技术[4]与线性数学约束的一些专门决策程序的集成一个与我们有关的工作，但仍然限于定时系统，是[17]。在目前的工作中，如第4.2节所解释的，我们已经扩展了编码，以处理混合系统。我们的混合系统模型与[10，13]中提出的线性和矩形混合自动机模型密切相关，主要区别在于实值变量动态的定义在[10]中，实值变量的动力学（称为波动条件）是通过对这些变量的一阶导数的线性约束来定义的，而在我们的模型中，动力学可以通过时滞的线性函数来表征，它直接约束变量的行为。这种方法类似于限制实值变量的连续流保持在矩形区域内，如[10]的矩形自动机模型。事实上，如[12]中所述，在凸线性约束下工作的假设下，要求在矩形区域内的包络等于要求在相应的分段线性包络内存在光滑函数文[14]提出的混合I/O自动机模型具有足够的一般性来适应我们的混合自动机模型离散和连续通信分别通过共享操作和共享变量来实现。然而，离散事件不允许改变共享变量的值，就像我们的例子一样。作为验证混合系统的另一种方法，我们引用[15]，其中提出了CHECK MATE工具。CHECK MATE使用称为商转移系统的有限状态近似来执行混合系统的验证。虽然这种方法不限于线性混合自动机，但验证分析可能是不确定的，在这种情况下，可以尝试对当前近似进行改进在[16]中可以找到对混合系统模型检查ESACS [6]项目（见http://www.esacs.org）是一个欧盟赞助的项目，其主要目标是定义一种方法和一个共享的环境，以改善复杂系统开发的安全分析实践。二次电源系统[5]是ESACS研究的案例之一。我们研究的主要动机之一是认识到，基于实变量离散化的传统有限状态模型检查的使用在处理混合系统的复杂性方面非常困难[5]。实际上，结果可能取决于离散化的步骤，以及状态爆炸G. Audemard等人/理论计算机科学电子笔记119（2005）1731这个问题使得这种方法在实践中不可行。7结论和今后的工作在本文中，我们讨论了自然建模为线性混合自动机的工业系统的验证问题。该方法是对文献[3]中提出的时间系统有界模型检验方法的一种改进 获得了效率通过使用MathSAT求解器。主要的限制是由分析类的不可判定性和实变量动态线性的约束。尽管如此，然而，这种方法使我们能够建模和分析系统的实际相关性，HY TECH目前无法处理。在未来，我们将通过扩大我们比较的工具集（其中一些在第6节中引用）和要分析的案例研究集，提供更全面的实验评估。关于SPS示例，我们计划在不同的粒度和抽象级别（例如，系统的双边模型）。我们将研究如何在这些特定问题上优化MathSAT求解器（例如，通过以[9，18]的风格约束分裂变量），并将尝试不同的编码。 作为连接的第一步 有界模型检查和无界验证之间的差距，归纳推理技术，以证明不变的属性将被调查。我们计划在不久的将来解决的一个重要问题是参数分析，这是目前在HY TECH支持。为了你，参数分析将允许我们在prop中替换恒定值sg1带一个参数α的P1（见第5节），以找出该性质是否成立的参数约束。最后，在未来，我们计划将该框架扩展到以完整的LTL表示的属性引用[1] Gilles Audemard，Piergiorgio Bertoli，Alessandro Cimatti，Artur Korni-lowicz，and RobertoRuptiani.基于SAT的布尔和线性数学命题公式求解方法。在Andrei Voronkov，编辑，CADE-18：自动演绎会议，LNAI第2392卷，第195-210页，丹麦哥本哈根，2002年斯普林格。[2] Gilles Audemard，Piergiorgio Bertoli，Alessandro Cimatti，Artur Korni-lowicz，and RobertoRuptiani. 集 成 布 尔 和 数 学 求 解 ： 基 础 ， 基 本 算 法 和 要 求 。 在 Jacques Calmet ， BernardBenhamou，Olga Caprotti，Laurent Henocque和Volker Sorge，编辑，CALCULEMUS-2002：符号计算和机械化推理集成研讨会，LNAI第2385卷，第231-245页，法国马赛，2002年。斯普林格。32G. Audemard等人/理论计算机科学电子笔记119（2005）17[3] Gilles Audemard，Alessandro Cimatti，Artur Korni-lowicz，and Roberto Pastiani.时间系统的有界模型检验。在Doron A. Peled和Moshe Y. Vardi，editors，FORTE 2002：Conference onFormal Techniques for Networked and Distributed Systems ， Volume 2529 ofLNCS ，Houston，Texas，November 2002.斯普林格。[4] A. Biere，A. Cimatti，E.M. Clarke和Y. 竹 没有BDD的符号模型检查。In R. Cleaveland，编辑 ， Proc.5th International Conference on Tools and Algorithms for Construction andAnalysis of Systems（TACASSpringer-Verlag，1999.[5] M. Bozzano，A.卡瓦洛，M。奇法尔迪湖Valacca，和A. 菲奥丽塔别墅。 改进复杂系统的安全评估：工业案例研究。在Proc. Formal Methods Europe（FME 2003），LNCS第2805卷，第208-222页，2003年[6] M. Bozzano，A. Villafiorita，O. P.kerlund，P. Bie b er，C. Bougnol，E. Bode，M.BretsCHneider，A. 你好，C。 卡斯特湾Cifaldi，A. Cimatti，A. Gri laut，C. 凯伦湾 L a wrence，A. Lüudtke，S. 梅特杰角帕帕佐普洛斯河Passarello，T.Peikenkamp，P.埃里森角塞甘湖特洛塔，L. Valacca和G.萨格勒布 ESACS：设计与安全分析的综合方法复杂的系统。 在欧洲安全和可靠性会议（ESREL245.出版社：2003年。[7] F.科普蒂湖菲克斯，E. Giunchiglia，G. Kamhi，A. Tacchella和M.瓦迪在工业环境中使用有界模型检验的好处。在Proc.CAVSpringer，2001年。[8] M.戴维斯，G。Longemann和D.洛夫兰 一种用于定理证明的机器程序。 ACM杂志，5（7），1962年。[9] E. Giunchiglia，A. Massarotto和R.阿提亚尼行动，其余的将遵循：利用规划中的决定论作为满足。在Proc. AAAI[10] T.A.亨辛格混合自动机理论。在Proceedings 11 th Annual International Symposium on Logicin Computer Science（LICSIEEE计算机学会出版社.[11]T.A. Henzinger，P. H. Ho和H.王台 HyTech：混合动力系统的模型。技术转让软件工具，1：110[12] T.A. Henzinger，P.W. Kopke，A. Puri和P. Varaiya。混合自动机的可决定性是什么？Journal ofComputer and System Sciences，57：94[13] T.A. Henzinger和R.马宗达 矩形混杂系统的符号模型检验。 In S. Graf和M. I. Schwartzbach，编辑，Proceedings 6th International Conference on Tools and Algorithms for Constructionand Analysis of Systems（TACAS史普林格出版社[14] N.林奇河，巴西-地Segala和F.凡德拉格混合I/O自动机。信息与计算，2003年。地出现。[15] B.I. Silva，K. Richeson，B.H. Krogh和A.楚提南基于CheckMate的混合动力系统建模与验证在Proc. ADPM 2000中，混合过程的自动化：混合动态系统。Shaker Verlag，2000年。[16] B.I.席尔瓦岛Stursberg，B.H. Krogh和S.恩格尔对混合系统验证的数学方法现状的评估。第40届决策和控制会议程序，2001年。[17] M. Sorea时间自动机的有界模型检测。在会议记录第三次研讨会上的模型时间临界系统（MTCS[18] 奥弗·斯特里克曼为有界模型检查调整SAT检查器。在Proc.CAV00，LNCS的第1855卷，第480斯普林格。