Moore机的硬件设备增量设计方法及应用于总线协议转换器的非回归分析简化系统和公式

理论计算机科学电子笔记128（2005）263-278www.elsevier.com/locate/entcs增量设计过程C'ecil eBraunstein1EmmanuelleEncrenaz2LIP6Universit′ePier eetMari eCurie，CNRSUMR7606Paris，France摘要本文形式化了一种增量式的方法来设计由Moore机描述的面向并行控制的硬件设备。该方法是基于新的行为，以建立一个更复杂的一个简单的设备连续添加 添加的新行为不得覆盖之前的那些一组CTL公式被分配给设计的每个步骤。两个连续设计步骤的公式之间的联系被形式化为一组公式变换F，说明：CTL公式f在步骤i的设计上满足，i ∈F（f）在步骤i+1扩展的设计上满足。这一结果已被应用在总线协议转换器的设计过程中的非回归分析的上下文中。在特殊情况下，它也可以用来简化系统和公式。关键词：系统设计与验证，仿真关系，计算树逻辑。1介绍本文源于对一些硬件组件可能设计方式的观察在某些情况下，硬件设计师可以采用递增策略：在定义了设计的信息流、数据路径和控制部分的粗略结构之后，他们开始实现最简单的情况，直到最复杂的情况。这是通过向现有功能添加新功能来实现的，1电子邮件：cecile. lip6.fr2电子邮件：emmanuelle. lip6.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.016264C. Braunstein，E. Encrenaz/理论计算机科学电子笔记128（2005）263-278一个越来越复杂的装置这对于实现流水线流程的设备尤其如此：可以粗略地绘制流水线的阶段，然后添加停止动作（例如，由于高速缓存未命中、连续指令之间的寄存器依赖性或异常处理而导致的停止动作）。通常，此类设备的验证通过模拟测试用例来执行。通过一系列表示为CTL公式的特性来指定组件，并通过符号模型检查[2]进行验证，这是一种补充模拟的验证方法例如，总线协议可以通过CTL公式来表示，并且可以通过将被测设计插入模仿总线的验证环境中来检查符合该协议的新设计，然后检查所有属性的规格进行验证。一般来说，增量设计方法不保留从简单组件到更复杂组件的属性集。一旦行为被添加到初始模型中，在初始模型中为真的全局属性在扩展模型中可能是错误的。因此，局部和全局属性（关于插入由其他组件组成的复杂环境中的组件）必须针对设计的每个增量步骤进行重新调整。这种增量设计过程是对[11]中应用细化策略的过程的补充。在细化策略中，首先定义全局信息流，所有情况，从最简单的到最复杂的，都是通过对初始模型的增量细化来获得的。每一次改进都被视为迈向真正实施的一步。这些方法的优点在于在精化过程中保持全局性质：如果一个性质在给定模型中为真，那么，如果精化是定义良好的，精化后的模型将保持初始性质。这导致了一种设计方法，确保实现尊重规范的属性。但这种细化策略排除了在设计过程中添加新功能：细化是对一组预定义行为的专门化，而增量方法是建立在添加新行为的基础上的。在我们的情况下，付出的代价是缺乏财产保护。几个增量相互干扰的方式已经在测试或软件插件中检测特征不一致的背景下得到了广泛的研究。例如，Plath和Ryan在[15，16，4]中提出了一种与模型检查器耦合的特征集成自动化工具（[16]用于Promela/SPIN [10]，[15]用于SMV [13]和[4]用于MOCHA [1]）。几个添加的特征之间的不一致通过LTL或CTL属性冲突来检测。[4]在《易经》中，有一种说法是：C. Braunstein，E.Encrenaz/理论计算机科学电子笔记128（2005）263265限制类型的功能。其他人，如Cansell和Mery在[3]中提出了一种方法来组合集成到Atelier B工具中的功能[5]：这里，应用细化策略来保证关于基本组件加上附加服务的抽象规范的实现的正确性。服务之间的不一致表现为不可证明的证明义务。我们的目的与[3，15，16，4]中描述的目的不同，因为我们的增量定义比他们提出的特征集成简单得多。因此，我们的增量是单调的：没有行为的覆盖但在简单模型中为真的CTL公式可能被增量证伪。我们的目标是构建一组CTL公式，通过重用简单组件的规范（并为添加的行为添加新的属性）来表示复杂组件的规范。我们感兴趣的是探索在初始模型中为真的属性和在扩展模型中为真的属性之间的联系。 这可以表达为：“我们可以将在初始模型中为真的CTL公式转换为在扩展模型中为真的其他CTL属性，从而捕获执行扩展的方式吗？”如果我们能做到这一点，我们就能确保扩展后的模型保留在初始模型上检查过的行为相反，从复杂模型上满足的一些性质，我们是否可以推导出一个更简单的性质来验证更简单的性质？给定一个加性增量，初始模型和扩展的，我们证明了这种CTL变换是可能的。变换后的CTL公式应用于扩展模型，将验证状态空间遍历限制在与初始模型导出的子图同构的子图上。这保证了，如果扩展模型遵守扩展规则，则应用于扩展模型的变换的CTL公式的验证结果与应用于初始模型的初始CTL公式的验证结果是相同的。本文的组织如下：在第一部分中，我们介绍了如何将新行为添加到现有模型中。第二部分给出了由初始模型和扩展模型导出的Kripke结构，并刻画了扩展模型的主要性质。基于这些考虑，第三部分给出了CTL公式的一组变换，将扩展模型的Kripke结构中CTL公式的验证限制在它所包含的初始模型的Kripke结构中。 然后，在第四部分中，我们介绍了在协议转换器的增量设计过程中应用这些转换的方式-在VCI（虚拟）266C. Braunstein，E. Encrenaz/理论计算机科学电子笔记128（2005）263-278组件接口）[6]和PI总线[14] -最后在第五节中我们得出一些结论。2增量形式化在本节中，我们将形式化正在设计的组件和增量。然后，我们描述了扩展组件。将元件看作是驱动数据通路的控制部件，其状态空间用一个完备的确定性同步Moore机来建模。该组件提供了一个由定向类型信号组成的接口。2.1信号和配置的定义定义2.1每个信号由一个名称s和一个有限的定义域Dom（s）定义。定义2.2设E是一组信号。C（E）是一个向量它将E中的每个信号与其定义域的一个值相关联。所有构形c（E）的集合称为C（E）。2.2组件的定义我们的方法迭代地将增量应用于组件W以构建更复杂的组件，其中Wi指的是由i个连续增量产生的组件。定义2.3一个分量Wi=被描述为一个确定的完全Moore机：Si：状态的有限集合。Ii：具有其有限定义域的输入信号的有限集合{（sigin，Domi（sigin））}Oi：具有其有限定义域的输出信号的有限集合{（sigout，Domi（sigout））}Ti：满足以下条件的有限转移集<$Si×C（Ii）×Si：<$s∈Si，<$c∈C（Ii），快！SJ∈Sis.t.（s，c，SJ）∈Ti（τ！”（“只有一个”）。L1：生成函数的向量={10，. ，l|O我|−1}，每个函数在每个状态下定义一个输出信号的值;对于所有输出信号o j0≤j<|O我|我们有l j：Si→ Dom（o j），si∈Si：初始状态C. Braunstein，E.Encrenaz/理论计算机科学电子笔记128（2005）263267注2.4将生成函数的向量应用于给定的Si产生一个构形c（Oi）。2.3增量增量是应用于组件架构的一组修改，以构建更复杂的组件。 它反映了执行在组件的接口上创建一个新事件。Wi的体系结构不考虑这个新事件的发生，而Wi+1的体系结构考虑了。事件是一种输入配置，它可能会导致系统增量是一个新事件（或一组新事件），引入新行为。一个新的事件可能以不同的方式发生：• 扩展一个或多个现有信号的定义域。组件的接口是固定的，但增量设计过程会考虑以前未考虑的这些接口的值。• 或者添加一个或多个新信号（具有定义域）。这是组件的数据路径的复杂性增加的情况在这两种情况下，新事件都是通过在输入信号集合Ii+1中出现新符号e来建模的，定义域为Dom（e）。该域被分成两个不相交的集合：安静值集合（VQT（e）），对扩展或添加的信号的配置进行分组，这意味着新事件尚未发生;活动值集合（V ACT（e）），对扩展或添加的信号的配置进行分组，这意味着新事件发生。命名e=val qt意味着扩展信号分别呈现属于V QT（e）的配置，e=val act属于V ACT（e）。新事件引入了新的转换和状态：新的行为被表示为前一个Moore机器中的新转换和状态。保留了Moore机的完备性和确定性新事件驱动新动作：一个或多个现有输出信号的域被扩展，或者一个或多个新输出信号被创建。如前所述，这些修改通过新输出信号o的出现进行建模，定义域Dom（o）分为V QT（o）和V ACT（o）不相交集。新的信号o被添加到旧的摩尔机器中存在的状态中，驱动其安静值之一，并且它出现在新鲜的状态中。状态，驱动其安静或活跃值之一。图1给出了一个可接受的增量。在左侧，描述分量Wi= ns的摩尔机对268C. Braunstein，E. Encrenaz/理论计算机科学电子笔记128（2005）263-278Fig. 1. 增量示例右边是分量Wi+1，由Wi随附加输入信号j的递增和Dom（j）={ 0， 1}产生;其安静值为0，其活动值为1。在Wi+1中，j的安静值标记了Wi中的所有转换;从Wi中存在的状态离开的新转换被标记为j的活动值;新状态是标记为j的活动或安静值的转换的源。定义2.5从一个分量Wi开始的增量是一个4元组INC=I+，R+，O+，O+>n+：新的可实现状态的集合，其中n+ni=nR+：新跃迁s<$（Si×Si）<$（Si× <$+）<$（<$+ ×<$+）<$（<$+×Si）的选择，其中R+<$Ti=<$.I+：新输入信号的选择及其定义域={（sig in+，Dom（sig in+））}。我们将等式设为I+，e={sigin+}，并且C（e）=V QT（e）=V ACT（e），使得：• Ti中的每个转换（s1，c，s2）将使其输入配置扩展为与新输入信号相关的子配置，V QT（e），表示为cJ= c，其中e =val qt。• R+n（Si× n+nSi×Si）中的每个跃迁（s1，c，s2）都将使其输入配置扩展为与新输入属于V ACT（e）的信号，由cJ= c表示，其中e= val act。O+：新输出信号的集合及其定义域=（o，Dom（o）），其中：Dom（o）=V QT（o）<$V ACT（o），使得与o相关联的输出函数针对W i中的所有状态返回V QT（o）中的值。通过对分量Wi应用增量而获得的分量Wi+1=Si+1，I i+1，Oi+1，Ti+1，Li+1，si>保留了Wi中存在的所有行为，假设在Wi+1中，新事件被维持到以下之一：，我们推导出Kripke结构K（Wi）=SK（Wi），sK（Wi），0，APK（Wi），LK（Wi），RK（Wi）其中：SK（Wi）=Si×C（Ii），sK（Wi），0={si} ×C（Ii），APK（Wi）=Ii<$Oi，LK（Wi） ={100，...，10|O我|−1} .{110，.，l I|我我|−1};RK（Wi）<$SK（Wi）×SK（Wi）且<$（s，ci）∈SK（Wi），<$（sJ，cJ）∈SK（Wi），我们有（（s，ci），（SJ，CJ））∈ R K（W）i <$（s，ci，SJ）∈ R.我我将增量应用于分量W i产生分量W i+1。在Kripke结构上验证了与Wi相关的CTL公式270C. Braunstein，E. Encrenaz/理论计算机科学电子笔记128（2005）263-278我S1C1CN......CIS2c'1...c'pS1c1图二. Moore机到Kripke结构K（Wi）.我们可以通过应用定义3.2从分量Wi+1导出Kripke结构K（Wi+1）。我们现在感兴趣的是描述K（Wi+1）相对于K（Wi）的性质，即表明K（Wi）包含在K（Wi+1）中，K（Wi）中存在的所有状态都标记有新事件的安静值3.1K（Wi+1）的性质通过构造，K（Wi）的行为树被保持在K（Wi+1）中，并标记有新事件的一些安静值。这种保持性可以表示为状态之间存在模拟关系的Kripke结构从两个连续的组件。更准确地说，丰富关系捕捉到这样一个事实，即前一个组件的行为包含在新组件中，并使用分配给其一些安静值的事件进行标记。对于所有的状态si=（s，c）∈K（Wi），设有SJ=（SJ，CJ）且SJJ=（SJJ，CJJ）∈K（Wi+1）使得：我我如果e = val qt，则SJ= s，CJ=c;如果e=val act，则sj= s，CJ=c。然后，SJ和s“i被说成是充实s i（在第一种情况下是（e = val qt））。命题3.4K（W i+1）的每个初始状态都用（e = val qt）来充实K（W i）的初始状态，模拟后者。证明（草图）：我们定义ρ KW S K （Wi）×S K （Wi+1），使得对于所有s∈SK（Wi），c∈C（I i），SJ∈SK（Wi+1），cj∈C（I i+1），则有（s，SJ）∈ρKWi<$（s = SJ，CJ= c）其中e = valqt. 通过构造，ρ KW是一个模拟关系。注3.5由上表，我们得出：如果sJ用e=val qt充实s，则sJ模拟s。如果sJ用e =val act充实了s，这并不意味着sJ模拟了s。如果SJ模拟了s，这并不意味着SJ丰富了s。...S1ci...S2c'1...S2c'iS1cnC. Braunstein，E.Encrenaz/理论计算机科学电子笔记128（2005）263271我0K（ W），0i+100推论(i) 如果在K（Wi）中存在某条无限路径，那么在K（Wi+1）中存在某条无限路径，事件e沿着该无限路径总是有一个安静值。如果σ= s0... sn. 在K（W i）中，则<$σJ=sJ. sJ... 单位：K（Wi+1）0n使得所有sJ都用（e =val qt）来充实s i。(ii) K（Wi）是K（Wi+1）中的最大子图，可从SJ到达，当e保持在其安静值之一时，它用（e = valqt）丰富s0（在K（Wi）中）。(iii) K（Wi+1）中的态是通过对K+中的态展开得到的，仅从初始状态sJ可达，该初始状态使sK（Wi），0增加a至少有一个状态被标记为（e =val act）的路径。(iv) 如果 SJ∈K（Wi+1）用（e = valqt）充实s∈K（Wi），则对所有的TJ∈K（Wi+1）使得SJ→TJ，存在t∈K（Wi）使得TJ由t的增量展开产生，并且s → t.证据(i) 通过对σJ的长度的归纳。(ii) 通过构造K（Wi+1），我们有SJ增加了s0，因此sJ模拟s0。 由于推论（i），存在路径σJ= SJ.. sJ... 使得所有0n态在K（Wi）中富集一个态。 对于每个状态RJ∈σJ，RJ充实一个状态r在K（Wi）中，其中（e =valqt），令t'使得r j → t j且t j满足（e=val act），则t '不属于K（W i）。(iii) 从推论（二）。(iv) 设SJ∈K（Wi+1）使s∈K（Wi）具有（e =valqt）且SJ→TJ.假设tJ不是通过由于K（Wi）中状态t的增量而扩展获得的 通过构造，tJ由W i+1中的状态r的扩展产生，该扩展由标记为（e =val act）的跃迁达到。矛盾因此，K（W i+1）包含K（W i），并且K（W i）可以在K（W i+1）中被 检 测 到 ， 因为它是用（e = val qt）标记的最大连通子图。 这被包含在模拟中的富集关系捕获我 们 现在利用这个特殊性来建立在K（Wi）上验证的CTL公式和在K（Wi+1）上验证的其他一些CTL公式之间的联系。4CTL公式转换[12]和[8]给出了任意模拟关系下两个Kripke结构之间的CTL公式保持性结果我们回顾它们在我们的具体情况下取得的成果。272C. Braunstein，E. Encrenaz/理论计算机科学电子笔记128（2005）263-278K（ W），0i+1在[12]中，作者证明了ECTL3公式从K（Wi）到K（Wi+1）的保持性;在[8]中，作者证明了ACTL4公式从K（Wi+1）到K（Wi）的保持性我们提出的结果是不是基于保存的CTL片段之间的一个组件和另一个，包括它，而是转换整个CTL运营商，并提供一个双蕴涵之间的初始公式和转换。给定一个CTL公式Φ，我们将给出将在sK（Wi），0（简称s0）中为真的Φ变换为在s j中为真的Φ'的规则（简称为sJ）当sJ用（e =val qt）充实s 0时。0 0定理4.1设s∈SK（Wi），s' ∈ SK（Wi +1），使得s's，其中（e= val qt），对于任意原子命题p∈AP K（Wi），对于任意CTL公式Φ，χ和Ψ（以及它们在AP K（Wi）中的所有原子命题），s|= Φ惠s'|= Φ J，其中Φ J是通过递归应用以下公式获得的公式：转换：Φ= p惠Φ J= p。Φ=不优惠Φ J=不优惠Φ= EX优惠Φ J=（e = val qt）EX优惠Φ =EF惠Φ J= E（（e = val qt）U J）。Φ= EG惠Φ J= EG（（e = val qt）惠Φ J）。Φ = E U χ 惠Φ J= E（e = val qt）惠Φ J）U χJ）。Φ= AX惠Φ J=（e = val qt）AX惠J。Φ=AF惠ΦJ=AF（（e=/valqt）惠ΦJ）。Φ = A U χ 惠Φ J= A（e = val qt）J）U（（e/= val qt）χJ））。Φ= AG惠Φ J= A（e = val qt）惠Φ J）W（e/= val qt））。Φ = A W χ惠Φ J= A（JW（χj（e/= val qt）。W代表证明（草图）：变换基于将K（Wi+1）中探索的计算树简化为不考虑事件的有效值的子树。根据推论（ii），这个子图表示K（Wi）。通过在其定义中包括（e = val qt）约束，证明了对于应用于原子命题的每个CTL算子的变换。然后通过归纳公式Φ的长度来进行证明。上面列出的转换不会修改初始公式的结构：时态运算符的重叠被保留，因此3ECTL代表仅限于潜在模态的CTL。4ACTL代表仅限于通用模态的CTL。C. Braunstein，E.Encrenaz/理论计算机科学电子笔记128（2005）263273CTL公式（以叠瓦式时态运算符的数量来衡量）不变。将EF转换为EU或将AG转换为AW不会显著改变验证的复杂性，因为它们基于相同的定点计算。 该变换被转换为经典BDD二元运算所执行的命题运算（与，或，隐含，. . ）.我们实现了一个工具，可以自动转换CTL定理4.1中描述的公式。此工具获取一个包含一组CTL公式的文件和一个包含增量定义的文件，并返回转换后的CTL公式集。5实验我们通过在VCI-PI包装器的上下文中转换一个更简单的规范，来尝试自动构建复杂系统的一部分包装器是一种包装在IP核周围并实现给定接口的设备。在我们的上下文中，IP核应该是VCI兼容的[6]并且所考虑的包装器是VCI接口和PI总线协议之间的适配器[14];因此，我们能够通过PI总线连接各种IP核图三. 主包装器VCI和PI接口PI协议区分发起总线传输的组件（称为主机）和响应传输的组件（称为从机）。IP核可以具有主功能和从功能两者图3说明了VCI-PI主封装器必须处理的主要信号接口VCI传输如图4所示。 VCI启动器发送请求到VCI-PI-master-wrapper（1），它向总线仲裁器274C. Braunstein，E. Encrenaz/理论计算机科学电子笔记128（2005）263-278一cmd_ack = 1 ; cmd_val =1rsp_val = 1 ; rsp_ack =一个'cmd_ack = {0，1} ; cmd_val =1rsp_val = {0，1} ; rsp_ack =Bcmd_ack = {0，1} ; cmd_val ={0，1}rsp_val = {0，1} ; rsp_ack ={0，B'cmd_ack = {0，1} ; cmd_val =1rsp_val = {0，1} ; rsp_ack =Ccmd_ack = {0，1} ; cmd_val ={0，1}rsp_val = {0，1} ; rsp_ack ={0，C'目标可以强制收回pi_rsp ={RDY，WAIT，RTR}目标可能会强加等待状态pi_rsp ={RDY，WAIT}目标始终就绪pi_rsp =RDY引发剂可以强加等待状态启动器始终准备就绪考虑的事件类型：增量(2)当VCI-PI主包装器拥有总线（3）时，它通过PI总线将每个VCI请求信元传送到VCI-PI从包装器（4，5）。VCI-PI从包装器将PI信元翻译成要提供给VCI目标的VCI信元（6）。VCI目标将VCI响应发送到VCI-PI从包装器（7），VCI-PI从包装器（7）通过PI总线（8，9）响应VCI-PI主包装器。后者将PI响应转换成VCI响应并将其发送到VCI发起者（10）。在某些情况下，VCI-PI从包装器可以实现前瞻机制，以便在一个周期中将响应发送到见图4。 平台和VCI传输使用增量设计过程的方法，我们开发了一套六个主VCI-PI包装，从一个非常简单的假设，VCI发起者和PI目标将始终在一个周期内响应，最复杂的一个支持延迟和收回事件发送的VCI发起者或PI目标。6个主包装器的层次结构如图5所示。图五.分层VCI-PI包装器。添加的每个事件对应于一个或多个信号的定义域的扩展。最简单的包装器（模型A）的行为是一个3级管道，C. Braunstein，E.Encrenaz/理论计算机科学电子笔记128（2005）263275同时执行：• 接受从其VCI接口发送到PI的VCI请求k• 在其PI接口上发送与第k-1• 在其PI接口上接受对第k-2个VCI请求的PI响应进一步的模型（B到六个主包装器的增量数据路径在图6中呈现，示出了通过从A到C '的增量排序连续添加的行为PI−Bus接口PI_D_INPI收缩启动器等待VCI接口RSPDATAPI_GNTPI_ACK[fRtr cmd_f fRtr_OKRSP_SAVEFSMRSPVALRSPACKRSPEOPCMDACKCMDVALNOPTRA_DA TRA_ADRGETDGETXRTREP装饰PI_D_OUT[ST Y XCMDCMDDATA中文（简体）PI_ADPI_OPCNOPPi缩回YXCMDADDCMDEOPPI等待见图6。 主包装器C '的数据路径。每个区域对应于不同的增加增量。我们在同步Verilog中实现了一个如图4所示的平台.我们使用VIS验证工具验证了该系统[7]。我们检查了主包装器B、从包装器B和整个系统的大约80个CTL属性（当VCI启动器和目标可能生成延迟事件时）。以下是在B平台上检查的CTL属性的示例276C. Braunstein，E. Encrenaz/理论计算机科学电子笔记128（2005）263-278#检查PI总线仲裁器和主封装器之间的接口。#属性1：# AG（（wrap0.state = R_bits）->（A（（m_pi_req=1） U（m_pi_gnt =1））））;#检查从包装器的行为（它的两个自动机#同步良好）。#属性2：#！EF（（wrap_cible.cmd_cible.state=CMD_IDLE）*！(wrap_cible.rsp_cible.state=RSP_IDLE））;#检查整个系统的行为：检查VCI发起方接收到的#个确认信元的数量是否等于它之前发送的#个请求信元的数量。#这里，发起者发送2个请求。 #属性3：#AG（（m_cmd_plen[6：0]= 8*m_cmd[0] = 1）->A（A）（(A(（m_cmd_plen[6：0] = 8 * m_cmd[0] = 1 * m_cmd_eop = 0 *m_cmd_val = 1）U（m_cmd_ack=1））U（ A（（m_cmd_eop= 1 * m_cmd_val=1）U（m_cmd_ack=1）int n= nums（nums = nums）;我们将定理1中描述的变换应用于模型B的80个CTL性质，其中增量将B变换为B '，并在现在包含B' VCI-PI主和从的系统上验证它们。验证结果成功，但验证时间增加，主要由于所验证系统的复杂性增加。当然，额外的CTL公式必须添加到对于一个小规模的系统（平台B和B'，有一个主包装器和一个从包装器），复杂模型的总验证时间增加了，但大部分时间都消耗在可达状态空间的构建过程中（5s vs 40s）。两个平台的属性验证额外成本具有相同的数量级（3s vs9s）。这些结果在中等规模的系统（平台B和B'，有两个主包装器和一个从包装器）中得到证实，其中B和B'验证时间之间的差距主要是由于系统复杂性的增加，而不是公式的复杂性，因为大部分验证时间都花在了可达状态空间的构建上（25 s vs 4 h）。一旦建立了可达状态空间，每个属性的验证对于B平台在10秒内执行，而对于B'平台在 20到50秒内执行C. Braunstein，E.Encrenaz/理论计算机科学电子笔记128（2005）2632776总结发言我们提出的CTL公式的转换规则是一种方法的基础，该方法可以从较简单的组件的规格中自动导出组件的部分规格。我们已经证明了这种方法可以在具体组件的设计过程中使用，假设增量遵守我们形式化的规则，因为我们利用了一个特定值的存在，该值标记了扩展模型中包含的模型的初始部分。变换后的CTL公式具有与初始CTL公式相同的复杂性（就CTL叠瓦算子而言）。实验结果表明，复杂系统验证时间的增加主要是由于可达性分析而不是CTL公式验证。我们打算朝着以下方向进行这项研究• 到目前为止，我们没有考虑到增加的所有特殊性;我们只考虑了一个特定事件的存在，该事件将状态集与初始模型中出现的状态和新的状态分开（该事件可能是由于现有信号域的扩展和/或新信号的添加）。我们没有利用增量的图形结构;大多数情况下，这个增量由添加一个新的状态（或一组状态）组成，这些状态表征了冻结等待某个继续信号被设置，允许数据路径继续。在这些情况下，一组新的CTL变换可以被定义，捕捉添加的行为。• 相反的分析也可能是有趣的：给定一个在复杂模型上验证的公式，我们能否找到一个增量（在本文中定义的意义上），使得复杂模型是从这个增量应用到一个更简单的模型中建立起来的如果是的话，我们是否可以将复杂模型的公式转置到一个更简单的模型上进行验证？验证将是部分的，因为它不会应用于复杂系统的整个行为集，但如果复杂系统太大而无法用经典的模型检查工具进行验证• 我们也有兴趣研究这种方法如何与假设保证验证过程相结合[9]。引用[1] R. T.A. A. Henzinger，F. Y. C. Mang，Shaz Qadeer，S. K. Rajamani和S.塔西兰MOCHA：Modularity in Model Checking。计算机辅助验证，第521-525页，1998年。278C. Braunstein，E. Encrenaz/理论计算机科学电子笔记128（2005）263-278[2] J. R. Burch，E. M. Clarke和K. L.麦克米兰符号模型检查：1020个状态及以上。 Informationand Computation（Special issue for best papers from LICS90），98（2）：153- 181 ，1992.[3] D. CcanselllandD. 我很好。数据的提取和重新定义。 在美国。 吉尔莫尔和M. R yann，编辑，用于设计功能的语言构造。斯普林格，2000年。[4] F.卡塞兹湾瑞安和P-Y。朔本斯用交替时序逻辑证明特征的非交互性。In S.Gilmore和M.Ryan ，editors ，Language Constructs for Describing Features ，pages 85SpringerVerlag London Ltd，2001年。[5] 普罗旺斯地区艾克斯信息技术公司在Atelier B，Manuel utilisateur，版本3.5，1998中。[6] 片上总线开发工作组。VSI联盟-虚拟组件接口标准（VCI）。2000年第2版[7] VIS集团。Vis：验证和综合系统。 在计算机辅助验证国际会议上，计算机科学讲义第1102卷，第428Springer-Verlag，1996.[8] O. Grumberg和D. E.久了模型检查和模块化验证。并发理论国际会议，计算机科学讲义第527卷，第250-263页Springer Verlag，1991年。[9] T. A. Henzinger，S. Qadeer和S. K. 拉贾马尼 您的假设，我们的保证：方法和案例研究。在计算机辅助验证中，计算机科学讲义第1427卷，第440-451页Springer-Verlag，1998.[10] G. J. 霍尔茨曼模型旋转。 IEEE Trans. 23（5）：279 - 295，May 1997. 软件实践中的形式化方法[11] K.拉诺在B语言和方法中，实用形式化开发指南。Springer-Verlag，1996.[12] C.卢瓦索Graf，J. Sifakis，A. Bouajjani和S.本塞勒姆用于并发系统验证的属性保持抽象系统设计中的形式方法第6卷，第1-35页Kluwer，1995年。[13] K. L.麦克米兰 在Symbolic ModelChecking中Kluwer Academics Publishers，1993.[14] 欧洲项目开放微处理器系统倡议。PI总线标准规范（OMI 324），1994年。[15] M. C. Plath和M.D. 瑞恩一种用于promela的特征构造1998年的SPIN[16] M. C. Plath和M. D. 瑞恩 SFI：一个功能集成工具。 In R. Berghammer和Y. Lakhnech，编辑，系统规范、开发和验证的工具支持，计算科学进展，第201-216页Springer，1999年。