模型检测算法在模拟电路中的应用

理论计算机科学电子笔记153（2006）37-52www.elsevier.com/locate/entcs基于模型检测算法Darius Grabowski1德国汉诺威大学微电子系统研究所丹尼尔·普拉特2Infineon TechnologiesAG德国慕尼黑拉尔斯·海德里希3德国法兰克福/美因大学计算机科学研究所埃里希·巴克4德国汉诺威大学微电子系统研究所摘要在这篇文章中，我们提出了模拟电路的模型检查算法，使规范的时间约束。此外，介绍了一种用于定义基于时间的规范的方法。一种已知的用于集成模拟电路的模型检验的方法已经被扩展以考虑时间约束。该方法将使用三个工业电路。模型检查的结果将与模拟验证进行比较。关键词：模型检测，模拟电路，CTL，时间约束1电子邮件：darius. ims.uni-hannover.de2电子邮件：daniel. infineon.com3电子邮件：hedrich@informatik.uni-frankfurt.de4电子邮件：barke@ims.uni-hannover.de1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.02638D. Grabowski等人/理论计算机科学电子笔记153（2006）371介绍形式验证方法广泛应用于数字电路的设计验证。与数字域相比，模拟电路的形式验证仍在研究中。混合系统领域的一些方法是众所周知的：使用普通微分方程（ODE）的线性或分段线性混合系统可以根据可达性分析进行分析[9]。最近的方法也能够处理非线性方程系统[5]。在晶体管级描述的模拟电路必须用一个强非线性微分代数方程组来描述。这些电路类型的方法可以分为不变集计算/可达性分析[6]和模型检查方法[7，8]，使CTL类似的属性描述。到目前为止，后一种方法不适合验证时间约束。由于电路规范的主要部分包含时间标准，因此将模拟模型检查扩展到考虑时间约束对于未来的使用至关重要存在定义和检查实时属性的方法，例如时间自动机：TCTL（[2]）和更专用于数字电路延迟的方法：WQCTL（[4]）。本文提出的扩展是基于模拟电路的算法，在状态空间离散化和检查规范时考虑时间行为，扩展计算树逻辑（CTL-AT）。本出版物的第一部分侧重于模拟模型检查的算法和验证时间约束的方法。新算法的功能将在本文的第二部分使用三个模拟电路块进行演示。2模型检测本文提出的方法是针对非线性动态模拟电路的分析基于扩展的修正节点分析[10]，为电路建立了一个非线性微分代数方程系统能量存储元件的状态变量（电容处的电压、通过电感器的电流）被用作独立变量。这些变量和输入变量跨越扩展的状态空间。在[7，8]中，提出了一种模拟模型检查方法，用于将CTL表达式表示的规格与电路行为进行比较。为了使这成为可能，连续的n维状态空间必须被映射到一个有限的离散过渡系统。因此，状态空间是有界的，并自动划分为有限个n维超盒。每一个超盒都代表着D. Grabowski等人/理论计算机科学电子笔记153（2006）3739发送状态空间的齐次部分，并被视为简化系统的离散状态图1a）示出了阻尼谐振电路的离散状态空间离散超盒的有限集合完全覆盖有限的状态空间。为了获得离散状态之间的后继关系，在状态空间的每个超盒内放置恒定这些点中的每一个通过其坐标表示输入和状态变量的值的组合通过数值求解电路的非线性DAE系统，可以获得这些点的解向量。通过使用过估计估计，可以将向量转换为离散状态转换在图1a）中，解向量如箭头所示此外，在放大的框内，深灰色超框的结果状态转换通过中点到中点连接可视化不同的标准在离散化过程中照顾到所产生的误差，并试图通过选择状态空间的适当细分来自动最小化误差。然后，可以使用数字模型检查算法来检查CTL-AT中制定的电路的规格2.1时间约束计算树逻辑时序行为的分析是基于计算树逻辑（CTL），如已经在数字电路分析中使用的[2，3，4]。在CTL的帮助下，可以定义有限状态机的规范。这些CTL表达式与系统行为的一致性CTL使用由所谓的路径量化器（A，E）和时间运算符（F-finally，G-generally，U-until）构建的特殊运算。路径量化器E定义了一个时间操作必须由有限状态机中的至少一条路径来完成A量化器确定CTL条件必须在所有可能的路径上满足时态运算符接受一个（F，G）或两个（U）状态集作为参数。所有CTL操作都会产生一组满足指定条件的状态一组状态用大写的希腊字母标记。使用时态操作可以描述状态机的动态指定。例如EF（Φ）导致最终到达集合Φ的路径的一组起始状态一个集合Φ的所有没有离开集合的路径的状态都可以通过使用CTL公式AG（Φ）找到。然而，这种基本形式的CTL既不适合分析模拟电路，也不适合指定时序行为。因此，该逻辑通过模拟运算符（>，）进行扩展，从而可以在模拟系统的连续状态空间要指定动态系统，请执行以下操作：40D. Grabowski等人/理论计算机科学电子笔记153（2006）37（a）（b）SEF[tlow，thigh]SEG[tlow，thigh]SE（ [tlow，thigh]SAF[t低，t高]SAG[tlow，thigh]SA（U [tlow，thigh]图1.一、 a）离散状态空间和b）CTL-AT参考为了使用CTL语法（CTL-AT）来描述时态行为，有必要引入时间约束的时态运算符，这些运算符额外地约束了操作的范围进一步的扩展涉及状态转换的方向因此，引入了时间反演，由-1运算符描述图1b）示出了模拟电路的CTL-AT操作。S表示自动机中路径的起始状态，该自动机满足每个图形下面指定的CTL-AT锥状形式描述了从S开始的路径的分支。与无约束操作相比，时间约束时态操作符F和U的使用导致结果集减少。所得到的状态集只包含那些在时间长度在操作给定的时间间隔内的路径上到达论证状态集的状态相比之下，G运算的时间约束增加了运算的结果集，因为G的先前含义从“通常”衰减2.2时间约束分析当考虑时间约束时，离散化状态空间中的延迟时间的识别是必要的。对于有限自动机中的延迟时间建模，有两种有前途的方法-时间自动机[1]和延迟状态转换。所提出的算法使用延迟转换来对所确定的转换系统内的时间进行建模，因为这在算法上更容易处理。此外，它们给出了模拟电路行为的良好近似延迟时间的计算发生在状态空间的离散化过程中。通过计算方程的时间步长t低t高t低t高t低不高t低不高t低不高特低不高D. Grabowski等人/理论计算机科学电子笔记153（2006）3741求解器在识别后续状态期间，获得延迟时间与解向量的长度的比率同时，所得到的过渡的延迟时间与两个状态的中点距离成比例地校正如果多于一个解向量导致相同的转变，则校正的延迟时间的算术平均值与转变相关联确定时间约束CTL操作的结果集需要在转换系统内处理时间路径长度。例如，其目的是找到在给定时间间隔内至少在一条路径上达到一组状态的所有状态（时间约束EF操作）。这些路径的结束由CTL操作的自变量确定，并且可以由状态空间的一组离散超盒组成利用CTL定理[8]，CTL-运算的计算可归结为两个基本运算EU和EG为了处理EF和EU运算的结果集，对前一算法进行了扩展，为每个状态分配一组离散的延迟时间。这个集合包含了从这个状态开始到目标集合结束的所有时间长度的路径。一条路径的总延迟时间是通过将其路径上所有转换的延迟时间相加来计算的。在完成算法之后，所得到的状态集被减少，减少的状态是在给定的时间间隔内没有延迟时间的状态（使用E-量化器）或在时间间隔外有一个延迟时间的状态（使用A量化器）。作为例子，我们将讨论计算时间约束EU操作的解的算法。然后，显示一个简单的示例（图2）来阐明功能。E（ΦU [tlow，thigh]）运算接受两组状态作为参数。所得到的集合旨在包含在给定时间间隔[tlow，thigh]内在Φ内的至少一条路径上达到Φ的所有状态该算法从被复制到中间状态集合Ω中的集合Ω开始。接下来，先前引入的延迟时间集合对于状态k初始化为零Ω通过重复添加满足以下条件的先前状态来收敛到结果集 到Ω，最后它必须满足上时间约束thigh。将状态添加到集合Ω导致在将所有包含的时间增加过渡时间之后，其延迟时间集合传播到前一个状态一旦找到不变集Ω，算法就终止结果集是通过最终将Ω减去所有不包含大于tlow的延迟时间的状态而获得的。42D. Grabowski等人/理论计算机科学电子笔记153（2006）37联系我们{3，5}一1B112D{1}2C{1，一1B112D{1}下2C{1，a）、{1}下一页1b）、{1}下一页1{0}{3，5}图二. a）过渡系统和b）方程（3）{A，B，C，D}（1）Φ={A}（ 2）Θ=E（θU[1，2]Φ）={C，D}（3）图2a）描绘了示例性转换系统以说明确定EU操作的结果的算法。除了转换，引用相应的延迟时间。每个状态节点包含转换到状态A时的可能延迟时间的集合等式（1）至（3）定义了两组状态和CTL-AT操作。结果集如图2b）所示。它只包含在1到2个时间单位的延迟间隔内至少在一条路径上到达的状态3基于时间的规范的验证方法在本节中，将介绍使用模型检查验证基于时间的规格（如信号边缘和振荡）的方法。使用模型检查而不是电路仿真的优点在于，通过使用模型检查算法和CTL-AT公式，可以证明系统符合其规范。3.1信号边沿的时间约束验证图3a）显示了信号边沿的瞬态曲线时间约束F运算可以应用于使用模型检查算法来证明上升时间为此，必须定义状态空间的两个区域Φhigh和ΦlowΦhigh和Φlow包含阈值的上侧和下侧的状态等式（4）和（5）用于通过使用模拟运算符（>，）和下限以及上限阈值来提取状态集合。在图3b）中，信号边沿在状态空间中绘制，其中电压U超过另一个状态变量X，该状态变量X对于该评估不感兴趣。Φ高=U>U高（4EED. Grabowski等人/理论计算机科学电子笔记153（2006）3743）Φ低=UU低（5）44D. Grabowski等人/理论计算机科学电子笔记153（2006）37高低指定的上升时间TLH可以通过等式（6）和状态组Φhigh和Φlow来验证。在应用模型检查算法之后，所得到的状态集合ΩLH包含在所有路径上从Φlow开始比TLH约束更快地到达区域Φhigh的所有状态。如果结果集为空，则指定不被电路填充ΩLH =AF[0，TLH]（Φ高）<$Φ低（6）a)b）、Ut t t图三. 正边缘：a）瞬态图和b）状态空间根据上升时间的结果，也可以使用公式（7）给出指定压摆率的对于下降沿，该方法也可以通过简单地互换Φ高和Φ低的设置以稍微修改的方式SR=U高-U低TLH（七）3.2振荡分析分析振荡行为的基础是提取振荡面积Θ。因此，状态空间被分成两个部分Φ低和Φ高。在下一步中，我们通过应用AF公式来确定在所有路径上最终分别导致Φ低和Φ高Θ是结果集合的叠加的一部分。应用AG公式，排除至少在一条路径上离开所选区域的所有状态。最后，我们使用逆EG公式来排除所有进入振荡的状态得到的公式在等式（8）中给出。Θ =EG−1（AG（AF（Φ））<$AG（AF（Φ）（8）在Θ内，可以选择两个部分Φ0和Φ1，将振荡区域分成正半空间和负半空间。在图4Θ中，Φ0和Φ1是不U百分之八十UD. Grabowski等人/理论计算机科学电子笔记153（2006）3745T+T在由状态变量X1和X2跨越的二维状态空间中示意性地显示。Ω01=E（ΘU[0，T高]Φ1）θΦ0（9）Ω10 =E（ΘU [0，T低] Φ0）<$Φ1（10）通过使用模型检查结合等式（9）和（10）中所示的时间约束EU操作，可以证明正半空间和负半空间的延迟时间T高和T低该过程相当于信号边缘的分析;唯一的区别是通过使用EU操作而不是AF来额外限制通向振荡区域的路径。见图4。 状态空间f=1不1=低高（十一）DC=T高T低+T高（十二）电路对特定振荡频率和占空比的顺应性可以从等式（11）和（12）导出。4应用建议的CTL-AT方法被实现为在汉诺威大学IMS开发的名为amcheck的前模型检查原型工具的扩展。所呈现的结果在具有sparcv9处理器的SUN服务器上处理。我们使用三个电路，分别包含两个三个状态变量。在这一点上，我们应该提到处理时间是一个关键问题，因为原则上它随着系统状态的数量呈指数级增长运行时的主要部分涉及状态空间的离散化，需要为每个超盒计算转换向量在最后一段中，我们给出了一些关于算法运行时间的信息。46D. Grabowski等人/理论计算机科学电子笔记153（2006）37VDDR2VDDR1+-Cloadv在VSS4.1施密特触发器第一个例子是图5a）所示的反相施密特触发器。电路的扩展状态空间由输入电压Vin和电容C负载两端的电压Vout跨越。运算放大器以静态方式建模，考虑输出节点的电压和电流限制。（a）（b）R3R4V输出图五. 施密特触发器：a）原理图和b）离散状态空间首先，我们必须定义状态空间的极限因此，我们评估由电阻R1. 四、运算放大器的电源电压（VDD= 5V和VSS=− 5V）会产生进一步的限制。因此，我们将限值设置为Γ：=[− 7 V. 7 V] × [− 7 V.. 7 V]。离散化状态空间如图5b）所示。状态空间包含两个准稳定区域，由vout= ±5V的小超盒表示。使用CTL-AT，我们确定了一些相关的量的施密特放大器，如下降时间，上升时间和转换速率。首先，我们通过等式（13）和（14）定义表示电压边沿的开始值和结束值的集合Φ low和Φ high。设定限值包含± 10%的公差。Φlow=vout<−4。5伏（ 13）Φhigh=vout>4。5伏（ 14）第一个分析涉及电路的上升时间应用等式（15）中的时间约束AF公式，我们得到包含具有以Φhigh结束的给定时间间隔的路径的所有状态。下降时间的相应分析将Φlow视为AF公式的源集（参见公式（16））。图6a）和b）显示了满足给定标准的集合。Ω LH= AF [0，1. 45· 10−6]（Φ高）（15）Ω HL= AF [0，1. 65· 10−6]（Φ低）（16）D. Grabowski等人/理论计算机科学电子笔记153（2006）3747（a）（b）图六、a）下降时间和b）上升时间的分析最后，我们必须检查满足等式（15）和（16）的结果集合是否与包含起始值的相应集合相交。 使用在等式（17 - 18）中，我们评估执行具有给定上升时间1的上升沿的所有状态。45·10 - 6s，另一方面，所有状态都在1中形成一个下降边缘。65·10−6秒。我们重新确定了列车运行时间然而，在实践中，它们由电路的规格给出。ΘLH = ΩLH低（17）ΘHL = ΩHL< $Φ高（18）图6a）和b）示出了满足等式（15）和（16）的结果集。黑色区域表示填充等式（17）和（18）的集合ΘLH和ΘHL模型检测仿真差异TLH<1.一、45μs1 .一、4μs3 .第三章。百分之五SRLH六、21V微秒六、43伏微秒3 .第三章。百分之四THL<1.一、65 μ s1 .一、6μs3 .第三章。1%SRHL五、46伏微秒五、63伏微秒3.0%表1模拟与模型检查48D. Grabowski等人/理论计算机科学电子笔记153（2006）37另一个表征施密特触发器行为的量是压摆率。它被定义为电压差和时间之间的比率。结果见表1，其中包含两种验证方法之间的关系模拟测量的上升时间为1. 4μs，而下降时间D. Grabowski等人/理论计算机科学电子笔记153（2006）3749微秒−1约为1. 6微秒。这些值证实了模型检查所获得的结果4.2运算放大器第二个应用介绍了晶体管级电路的压摆率验证我们使用图7所示的工业运算放大器。原理图包含电路本身（方框部分）以及控制输入和输出行为的输入电压是直流电源VDC和运算放大器正输入端的交流电压VIn的为了测量压摆率和过冲，我们将输出连接到负输入。电源电压VDD被设置为1。5伏。电路的状态空间由输入电压V In以及电容C load和C comp两端的电压V out和V comp跨越。VDDv在VDC见图7。 运算放大器运算放大器由两级组成。第一个是Differential对（P0，P1），有源负载（N0，N1）由电流源I偏置控制。第二级是由P2和N2构成的驱动级。为了改善电路的瞬态性能，增加了所谓的第一项测试检查运算放大器的压摆率。它至少应该是3。6V。我们使用的假设是，为了实现这样的压摆率，输出电压的上升阶跃必须在预定时间内完成。在这种情况下，我们使用从0开始的输入步长。3V至0。5伏。因此，最大时间这一步的花费必须是5。5· 10−8秒。该公式是为一个3-维扩展状态空间ΦUl ow=EG−1|vIn=c ons t. （v/n>0. 29V/VIn<0. 31V）（19）ΦUhigh=EG|vIn=c ons t. （v/n>0. 49伏，我没有<0。51V）（20）VSR|=EF[0，1·10−20]（AF[0，5. 5·10−8]|vIn=c ons t.（ΦU高hΦU低w））（21）VDDP4P3P2I偏置Rout在-P0P1voutC组分In+N2N0N1CloadR负载RIn+VSS50D. Grabowski等人/理论计算机科学电子笔记153（2006）37Θ= EG|（24）vIn=const.意味着由于输入变化而导致的转换被禁用。在转换中，使用关于EF[0，1·10-20]的表达式将输入jump转换为适当的值，而不改变其他状态变量。在1· 10−20s的极短时间内，状态变量的变化非常小。例19-（13使用此公式运行会产生一组非空的三个方框，表明满足压摆率规格。作为附加测试，给出了过冲规格Γ In=（v In>− 0. <0. 2伏）（22）r_Out=（v_Out> 0. 55 V直流输出<0. 95V）（23）−1DC vIn= const. 在Ω|=E（rU−1Θ）中文（简体）操作系统输入输出这些区域是针对设定电压VDC=0的输入和输出电压范围定义的。75伏。过冲表达式的结果集不为空。因此，该规范不成立。过冲的原因是电阻Rout与输出电容一起导致延迟反馈，最终导致过冲。4.3压控振荡器第三个例子是图8所示的压控振荡器（VCO）。对应的状态空间由电容C1和C2处的电压跨越。输入由理想电压控制电流建模，该理想电压控制电流由对电容C2充电的TN 1、TP 1、TN 2、TP 2、TN 5镜像。假设输出电压vC1为VDD，C2由通过由逆变器（TN4，TP4）控制的开关TN 3，TP 3的输入电流线性地充电。如果svC2超过S临界触发器的峰值阈值，由R1和R2确定，则vC1将变为VSS。因此，C2被放电直到达到初始状态，导致振荡。基于CTL-AT，我们检查VCO的两个属性第一个属性是某些不同输入电压的振荡频率使用结果，我们检查作为输入电压的函数的频率线性度。考虑到电源电压和电阻R1和R2的值，状态空间定义为r：=[− 3]。1V.. 3.第三章。1V] ×[− 0. 08伏.. 0的情况。08V]。图9a）显示了VCO的离散化状态空间。它包含一些水平的表示输出电压的最大值和最小值之间的快速转换的路径。振荡时间主要由vC1 = ± 2处的缓慢（垂直）跃迁决定。5伏。利用第3.2章中给出的方程（8），我们计算了振荡区域的所有状态因此，我们将给定的状态空间分成两部分，D. Grabowski等人/理论计算机科学电子笔记153（2006）3751VDDVDDVDDVDDTP1TP2R1VDDTP4TP3+-gvinTN4TN3C2R2VSSC1Tn5TN1TN2VSSVSSVSSVSS见图8。 压控振荡器a)b）、见图9。VCO：a）离散状态空间和b）振荡区域在围绕VC1=0V振荡的电路上的已知负载：Φ10w=vC10V（ 26）Φhigh=vC1>0V（ 27）图9 b）示出了表示在v in = 1处的振荡区域的状态集合。7V。此外，它还包含通过瞬态模拟计算的轨迹（黑色曲线）。可以看出，振荡区域与轨迹相交。如第3.2章所述，确定振荡时间的方法需要划分振荡区域。因此，我们定义了两个具有小范围的集合我们选择一个快速过渡的部分，以尽量减少离散化误差。包含振荡路径的起始区域的两个集合由等式（28）和（29）定义52D. Grabowski等人/理论计算机科学电子笔记153（2006）37Φ0=θ（vC1>0）（vC1<0. 05）C（vC2>0）（28）Φ1=θ（vC1>0）（vC1<0. （29）第二十九条第一款与第4.1章中使用EF运算来获得路径长度的方法不同，我们现在以迭代方式使用时间约束EU因此，我们需要一个时间上限来保证方程（30）的结果集与Ω10重叠，反之亦然。Ω 01= E（Θ U [0，0. 64] Φ1）（30）Ω 10= E（Θ U [0，0. （31）a）、0.08vC2-0.08b）、0.08vC2-0.08-3.1vC13.1-3.1vC13.1见图10。 VCO：a）左振荡路径和b）右振荡路径图10a）和b）示出了等式（30）和（31）的结果。在这个例子中，使用v in= 1。7 V，我们得到两个不同的时间延迟，由0. 64秒，0的情况。69秒。我们估计振荡时间约为1。33秒。值得注意的是，模型检查会高估时间延迟。然而，振荡区域的内部路径允许比外部路径更快的振荡回想一下，这个效果取决于离散化的精度。我们现在关注输入电压和振荡频率的线性度在这个例子中，我们估计振荡频率应用三个不同的输入电压由v in= [1]。7V，2. 2伏，2. 7V]。为了测量线性度，我们使用频率和输入电压的商定义线性度误差：Δf/Δvin。在表2中，我们将模型检查结果与瞬态模拟结果进行了比较频率偏差和数量的相对误差约为5%。相对线性误差测量为10。0%（瞬态模拟）和12。5%（模型检查）。最后，我们给出了一些信息的运行时所提出的例子我们考虑电路方程的数量。实际D. Grabowski等人/理论计算机科学电子笔记153（2006）3753模型检测仿真v在期间频率期间频率rel. 误差1 .一、7V1 .一、33S0的情况。75Hz1 .一、27S0的情况。79赫兹五、06%二、2V1 .一、01s0的情况。99赫兹1 .一、01s0的情况。99赫兹0的情况。百分之一百二、7V0的情况。83年代1 .一、20Hz0的情况。85后1 .一、17Hz二、百分之五十六表2模拟与模型检查每个框的相交深度取决于最大预定相交深度和方程系统的非线性。表3显示了运行时。所有电路的状态空间使用每个超盒的五个测试点进行离散化。通常，该算法的运行时间主要由状态空间的离散化，而CTL操作的评估具有可忽略的持续时间。比较施密特触发器和VCO，可以看出，由于数值求解器的缘故，跃迁的计算在很大程度上取决于方程的如前所述，运行时间随着状态变量的数量呈指数级增长，这可以在运算放大器示例中看到。该电路由51个方程描述，这与VCO类似。状态空间包含三个状态变量，产生58962个超盒，这比具有两个状态变量的VCO电路多约60倍。电路施密特触发器运算放大器VCO方程115155最大相交深度121614Hyperboxes1229589621267离散化时间20岁小行星2873414 s表3模型检查：5结论近年来，模型检测被成功地应用于验证数字电路，使得几乎完全自动化的验证成为可能。通过对模拟系统连续状态空间的离散化，提出了模型检验算54D. Grabowski等人/理论计算机科学电子笔记153（2006）37法。D. Grabowski等人/理论计算机科学电子笔记153（2006）3755RITHM也可以应用于模拟电路。一般来说，模拟系统的规格是基于时间约束的。因此，离散化算法已被扩展考虑延迟时间，稍后被建模为延迟状态转换。为了应用时间约束计算树逻辑（CTL-AT），已经开发了新的算法此外，还介绍了用于验证信号边沿和振荡的时间分析方法以三个电路为例说明了该方法的实用效果仿真结果与模型检测算法的比较表明，模型检测是一种自动验证模拟电路的好方法。引用[1] 巴尔河，时间自动机，CAV八比二十二[2] 巴尔河，C. Courcoubetis和D. Dill，Model-Checking for Real-Time Systems，LICS414- 425[3] 巴尔河，C. Courcoubetis和D. Dill，Model Checking in Dense Real-Time，Information andComputation（1993），pp. 2-34[4] Chatterjee，K.，P. Dasgupta和P. Chakrabarti，定量推理的分支时间时态框架，自动推理杂志，30（2003），pp. 205-232.[5] 天啊TA. Douze和O.Maler，Verification of analog and mixed-signal circuits using hybridsystem techniques，FMCAD 04：Formal Methods in Computer Aided Design（2004）。[6] Dellnitz，M.，G. Froyland和O. Junge，面向Gaio集的动力系统数值方法背后的算法，遍历理论，动力系统的分析和有效模拟（eds。B. Fiedler），Springer（2001），pp. 145-174。[7] Hartong，W.，L. Hedrich和E. Barke，Model checking algorithms for analog verification，DAC542-547[8] Hartong ， W. ， L. Hedrich 和 E.Barke ， On discrete modeling and model checking fornonlinear analog systems，CAV401-413[9] Henzinger，T. P. - H.何，非线性混杂系统的数学分析，CAV225-238[10] Ho ， C. ， A. Ruehli 和 P. Brennan ， 网 络 分 析 的 改 进 节 点 方 法 ， IEEE 电 路 与 系 统 学 报 22（1975），pp.504-509