基于次协调逻辑的模型检测方法研究与应用

理论计算机科学电子笔记157（2006）23-38www.elsevier.com/locate/entcs基于次协调逻辑陈东火1、吴金钊1、21中国科学院成都计算机应用研究所，成都6100412FakultüatfurMathematikundInformatikUniversitüatMannheim，D7，27，68131 Mannheim，Germany摘要经典逻辑不能用于有效地推理具有不一致性的并发系统（不一致性经常发生，特别是在开发的早期阶段，当开发大型复杂并发系统时）。在本文中，我们提出了使用一个次协调的时间逻辑（QCTL）支持验证的时间属性，这样的系统，即使在一致的模型是不可用的。我们引入了一个新的概念paraKripke模型，它抓住了QCTL蕴涵关系的次协调性质。在此基础上，我们探讨了QCTL模型检测的方法，并给出了实现QCTL模型检测器的具体算法。 在续集中，一个简单的例子，展示了如何利用所提出的模型检测技术来验证不一致并发系统的时间特性。保留字： 不一致性，并发系统，次协调时态逻辑，模型检测1介绍近年来，模型检测[1]已经成为一种自动验证有限状态并发系统正确性的成熟技术。该技术已有效地应用于硬件、通信协议、软件工程等的正确性推理。1Ema il：chendonghuo@hot ma il. COM1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.02124D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）23为了研究和实践的目的，已经开发了一些模型检查器，包括SPIN [2]和VIS [3]。尽管它们种类繁多，但现有的模型检查器通常基于经典逻辑，因此不能用于推理包含不确定或不一致信息的并发系统的规范。据我们所知，由于其表达能力和推理能力，经典逻辑对于并发系统和推理的规范的形式化表示非常有吸引力。不幸的是，不一致性导致了经典逻辑推理中的问题。在经典逻辑中，任何事情都可以从一组不一致的假设中得出，也就是说，不一致导致琐碎和无意义的推理。然而，在大型复杂并发系统的开发过程中，不一致性是不可避免的现象[4]。在需求工程中，模型经常是不一致的，因为它们结合了冲突的观点。在设计和实现过程中，集成由不同成员定义的组件时会出现不一致性。质量标准分析过程的很大一部分用于检测和消除此类不一致，因为传统上不一致被视为不可取的。但从始至终，特别是在早期阶段，保持绝对的一致性并不总是可能的。这通常是不可取的，因为这可能会不必要地限制开发过程，可能导致重要信息的丢失[5]。因此，已经有相当多的技术和工具的开发研究，为如何以更一般的方式管理不一致性提供了实际支持，并可能在存在不一致性的情况下进行推理[6，7，8]。次协调逻辑和多值逻辑[9，10]为我们提供了新的逻辑基础，适用于不一致推理。次协调逻辑[11，12]比经典逻辑弱，允许某些矛盾为真，通过逻辑连接词的非标准行为，通过限制证明系统等实现不一致下的非平凡推理。为了充分利用次协调逻辑，开发人员不必再粗略地拒绝任何不一致信息的系统规范，而是以更理性的方式分析它们。然而，目前很少有人尝试为不一致的模型开发自动推理工具，大多数工作仅限于次协调逻辑本身。一些值得注意的例外是Hunter，Nuseibeh和Riarka [7，13]，他们使用次协调逻辑QCL来推理演化规范。此外，根据Hunter等人提出的次协调逻辑QCL [7]的思想在本文中，我们提出了次协调逻辑称为QCTL通过扩展QCL的能力，指定时间方面的一致，D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）2325目前的系统。进一步，我们研究了次协调时序逻辑QCTL的模型检测问题。第二节简单介绍了QCTL语言。第三节详细讨论了QCTL的模型检测问题。为了激励我们的工作，第4节给出了一个例子，显示所提出的模型检测技术的模型检测的预期时间属性的不一致并发系统的权力。第5节对本文进行了总结。由于篇幅所限，所有相关的证明都被省略了。2次协调时序逻辑QCTL2.1语法QCTL的语法与CTL的语法相同，但在本质上有很大的区别。QCTL基于次协调逻辑方法论，而CTL基于经典命题逻辑。这一事实导致了证明系统和语义的巨大差异。临时操作符的介绍如下：−在下一个状态，-最终，Q-总是，U-直到。 此外，两个路径量化器E和A具有“有一条路”和“对于所有的路”的直观含义分别设P表示一组原子命题。QCTL的公式具有以下抽象语法，其中p在P上变化：α：= p |¬α |α1∧ α2|α1∨ α2|E（A）α |E（A）α |E（A）Q α |E（A）（α1U α2）设L表示上述抽象语法的公式集。此外，委员会认为，α→β通常是<$α<$β的缩写。 通常对于每个p∈ P，p或<$p称为文字。一个形式为l1的公式。。对于n≥1，n≥ 1称为子句， 其中l1，.，ln 都是文字。此外，委员会认为， 我们提供了一些基本定义，为后续工作做好准备。定义2.1.1对于α，β ∈ L，这种形式为σ（αUβ），<$σ（αUβ），σxα或<$σxα的公式称为拟文字，其中σ表示路径量化器E或A，x表示时间算子之一，Q，n。 我... ∨ l n∨ql1. 我们称m∈ L为拟子句，其中m ∈ L为拟子句. 1 ≤i≤n，l i是一个字面量，并且是ni。1≤i≤m，qli是一个拟文字。此外，子句或准字面量是特殊准条款因此，σ和x在上下文中具有上述含义，当它们没有被明确解释时。26D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）23定义2.1.2设F是通过有限地应用以下规则生成的最小公式集：1. 对于p∈ P，p，<$p∈F.2. 设α，β∈F，且α，β是两个拟子句，则α<$β∈ F.3. 对于α，β∈F，α<$β∈F.4. 对于α，β∈F，σxα，σ（αUβ）∈F.任何α = α1... 当n≥1时，<$α n∈F称为完全CNF，当1≤i≤n时，αi称为完全子句.定义公式集F的目的是帮助我们计算在QCTL上实现模型检验算法时所使用的一个重要的公式集Facts（α）（α∈ L），并建立一个简洁的证明。QCTL的证明系统QCTL具有与经典时序逻辑CTL相同的语法它在语义层次上与CTL不同。这正是使QCTL成为次协调逻辑的关键所在。2.2语义QCTL的动机是需要对具有不一致规范的并发系统进行推理真理或谬误的概念就这样被抛弃了。我们在这里将每个公式视为一个信念，遵循[7]中的思想QCTL通过解耦公式之间的关系实现了次协调方法以及语义层面的否定。为了达到这个目的，首先从原子命题的集合P构造一个肯定和否定对象的集合。对于每个p∈P，+p称为正对象，−p称为负对象。定 义 2.2.1 QCTL 中 的 正 对 象 和 负 对 象 的 集 合 定 义 为 O={+ p|p∈P}<${−p|p∈ P}。Kripke结构被广泛用作时态逻辑的语义模型，如CTL [14]。在这里，我们提供了一个新的语义QCTL扩展Kripke结构paraKripke结构。定义2.2.2元组M=（S，R，L）称为paraKripke结构，其中• S是一个非空的状态集。• R<$ S× S是一个全关系，这意味着对每个 s∈ S都存在 t∈ S满足（s，t）∈R.D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）2327• L：S <$→2O是一个标签函数，它用一组正或负对象来标记每个状态。ParaKripke结构与一般的Kripke结构相似，除了标签函数。但正是标签功能抓住了结构背后的基本思想。在paraKripke结构中，状态被标记为包括在O中的阳性或阴性对象。ParaKripke结构将被用作QCTL的语义模型。定义2.2.3设M=（S，R，L）是一个paraKripke结构。M的计算路径x被定义为x=（s1，. 我... . ），其中对所有i≥1，si∈S且（si，si+1）∈R. s1称为x的初始状态，并且（s1，. ，s k），其中k ≥ 1，x的初始前缀。在定义QCTL中的满足关系之前，我们首先提出了状态中文字信念的满足性概念对于paraKripke结构M=（S，R，L），设s∈S，Es=L（s），p∈P.（1）p满足si ∈ P+P∈Es，（2）<$P在si∈P∈Es中是可满足的.从上面的讨论中，我们看到paraKripke结构包含信念的概念，其中一个原子命题及其否定在同一状态下都是可满足的，也就是说，一个状态可以被标记为+p和−p，p∈P。因此，QCTL在语义层面上解释了公式与其否定之间的联系这使它成为一个次协调逻辑。为了实现不一致情况下的非平凡推理，QCTL的证明过程是一个两阶段的算法：分解步骤和合成步骤，从而避免了不一致情况下的平凡推理。细节可以在文件的完整视图中找到。为了抓住这个想法，我们需要为两个阶段建立两个满足关系，称为强满足关系和弱满足关系。强满足的概念对应于分解阶段，弱满足的概念对应于合成阶段。定义2.2.4设M=（S，R，L）是一个paraKripke结构。强满足关系|= ts定义如下：1. 对于原子式p，（M，s）|= tsp i +p∈ L（s）.2. 对于原子式p，（M，s）|= ts<$p i <$−p∈ L（s）。3. （男，女）|=ts α βi（M，s）|=tsα和（M，s）|=tsβ。4. 对于一个子句α= l1. 其中l1，. ， ln是文字，（M，s）|=tsαii.1≤i≤n，（M，s）|=tsl i和ti。1≤i≤n，（M，s）|=ts<$l i蕴含（M，s）|=tsDisj（α，l i），其中Disj（α，l i）是原始公式l1. 不带分离词li。28D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）235.对于一个拟子句α=l1<$... l n （M，s）|=tsαi（M，s）|=tsl1. 你是我还是你。1≤i≤m，（M，s）|=tsql i，其中l1，. ..，Ql，m是准文字。6. （男，女）|= tsE存在t∈S满足（s，t）∈R和（M，t）|= tsα。7. （男，女）|= tsA<$α i <$，对于所有t∈S，其中（s，t）∈ R，（M，t）|= tsα。8. （男，女）|= tsE <$α i <$i存在计算路径x =（s0，. ，sn，... ）与s0= s且mi，i ≥ 1，（M，s i）|= tsα。9. （男，女）|= tsA <$α i <$对于初始状态为s的所有计算路径，（M，s）|= tsEα10.（男，女）|= tsE（αUβ）i ||存在初始prefix（s0，.，sk），满足（M，sk）|= tsβ和（M，s i）|= tsα，对于所有iβ <$γ E'2. <$AαtE（<$α）E3.<$（α <$β）<$γ<$t（<$α <$β）<$γ E'3. <$EαtAQ（<$α）E4. α <$（β <$γ）<$t（α <$β）<$（α <$γ）E'4。<$AαtEQ（<$α）E5. α <$（β <$γ）<$t（α <$β）<$（α <$γ）E'5 。 <$E（αUβ）<$AQ（<$β）<$A（（αβ）U（β））E6. （α → β）γt<$α β γ E'6. <$A（αUβ）<$tEQ（<$β）<$E（（αβ）U（β））E7. <$（α→β）<$γ<$t（α<$$>β）<$γ至此，我们已经为定义蕴涵关系做好了准备|= tof QCTL.设2L表示L的幂集：定义2.2.7蕴涵关系|QCTL的= t定义如下：• |= t⊆(2L−∅)×L,where∅istheemp tyset.• 对于Γ ∈ 2L− ε和β ∈ L，|=tβi ≠ 0，对所有的仿Kripke结构M=（S，R，L）且s ∈ S，（M，s）|=tsα对所有α ∈ Γ蕴涵（M，s）|=twβ。蕴涵关系是次协调的。 在下一节中，我们将建立基于蕴涵关系的模型的新概念|= t，这样我们就可以采用自动模型检测技术来分析时间序列的在不一致的情况下并发系统的性质。3QCTL模型检验3.1方法如上所述，我们可以使用paraKripke结构对包含不一致信息的并发系统进行因为蕴涵关系|QCTL的= t被定义在一种模式中，与经典逻辑的模式非常不同，paraKripke结构不适合对不一致并发系统的规范进行建模，就像标准Kripke结构在[1，15]中所做的那样。30D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）23在下文中，我们建立了基于paraKripke结构的模型的概念，这与基于标准Kripke结构的模型不同。定义3.1.1设α∈L，元组M=（S，R，L，S0）是paraKripke结构，其中S0<$S是初始状态的非空集合。（M，s0）|= tα，对于s0∈ S0i，存在一个有限的公式集Γ L，它满足<$γ.γ∈ Γ，（M，s0）|= tsγ和Γ |= tα。 M 是αi ε的paraKripke模型s∈ S0，（M，s）|= tα。我们认为，根据定义3.1.1，直接将模型检测问题转换为推理问题是不可接受的。因此，接下来的工作集中在研究对QCTL进行模型检测的方法许多在经典模型检测方法中自然成立的断言在QCTL模型检测中是不明显的，甚至是完全不恰当的，即，通常，对于CTL中的时间公式α，α的模型意味着它不是一个α的模型。给定一个仿Kripke结构M=（S，R，L，S0），我们首先给出一些基本命题.命题3.1.1设l1，.，l，n（其中n≥ 1）是文字，并且ql，.，ql mform≥1个拟文字。 对于s∈S，1. （男，女）|= tl1. （M，s）|= tl1or. 或（M，s）|= tl n.2. （男，女）|=tl1。 . . 我不知道。 . . qlmi（M，s）|=tl1。 . . n，（M，s）|=tql1或者... 或（M，s）|= tql m.命题3.1.2设α，β∈ L.对于s∈S，1. （男，女）|=tα β i（M，s）|=tα或（M，s）|=tβ。2. （男，女）|=t α βi（M，s）|=tα和（M，s）|=tβ。3. 令α1=…当n≥1时，α n是α的完全CNF。（男，女）|=tαi（M，s）|=tα1和. 和（M，s）|=tα n。第3.1.2章并不意味着|= tα<$β必须得到Γ |= tα或Γ |= tβ。考虑对于p，q∈P，Γ ={p<$q}。显然，|= tp <$q，但r |tp和r |= tq.对于公式α，设F作用s（α）={αJ|（男，女）|= tsαJ蕴涵（M，s）|=twα}，直观地称为α的一组强因子。的详细定义F acts（α）将推迟到下一小节。命题3.1.3设α∈ L，s∈S。 以下内容成立：D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）2331s0S1S2S3Fig. 1. ParaKripke模型1. （男，女）|= tE t.t∈S，（s，t）∈R且（M，t）|= tα。2. （男，女）|= tE <$α i <$存在计算路径（s0，s1，. . ），初始状态s0= s，满足mi.i≥ 1，（M，si）|= tα。我们得到了关于paraKripke模型的一些基本结论，这些结论是实现具体算法的基础但到目前为止，我们还没有涉及对这些公式，如E（αUβ），AQα和Aα∈L的模型检验方法。由于QCTL蕴涵关系的次协调性质，使得这些公式的模型检验比传统的方法更加复杂和困难。Eα和Eα。现在我们来看看E（αUβ）。根 据 定义3.1.1，对于s∈S，（M，s）|= tE （ αUβ ） 意 味着 Γ <$L， <$γ.γ∈ Γ ， （ M ， s ） |= tsγ和 Γ |= tE（ αUβ ） 。 QCTL 的 证 明 系 统 确 定 了 一 定 存 在 E （ αJUβJ ） ， 满 足 E（αJUβJ）∈Γ，或者E（αJUβJ）是由Γ通过应用分解规则导出的，其中αJ∈Facts（α），βJ∈Facts（β）.换句话说，（M，s）|= tE（αUβ）i（M，s）|= tsE（αJUβJ）。根据传统观点，（M，s）|= tE（αUβ）i存在某个初始prefix（s0，.，sk），满足（M，sk）|= tβ和（M，s i）|= tα，0≤i< k。然而，这个结论在paraKripke模型的概念中是不正确的。让我们用一个例子来说明这一点。图1示出了具有初始状态s0的paraKripke结构M，其中L（s0）={+p，-q，-r，-pJ}，L（s1）={−p，+q，−r，−pJ}，L（s2）={−p，−q，+r，−r，−pJ}和L（s3）={−p，−q，+r，+pJ}对p，q，r，PJ∈ P.考虑时间性质E（p <$q<$r U pJ）。显然，对于0 ≤ i ≤ 2，（M，si）|= tp<$q<$r，且（M，s3）|= tpJ.但它不能导出（M，s0）|= tE（p<$q<$r U pJ）。事实上，F acts（p<$q<$r）={p，q，r，p<$q，p<$r，q<$r，p<$q<$r}。由图1可知，不存在任何fs∈ F act s（p <$q<$r），满足对0 ≤ i ≤ 2，（M，si）|= tsf s，换句话说，（M，s0）|= tE（p<$q<$r U pJ）。类似地，以泛量化器A和EQα开始的模型检验这类公式面临着与模型检验E（αUβ）相同的挑战：蕴涵关系的次协调性增加了模型检验这类公式的复杂性。ParaKripke结构削弱了否定算子<$的意义，因为α和<$α都是彼此唯一满足的。在QCTL上的模型检验中，（M，s）|= tα不否认（M，s）|=t<$α。因此，32D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）23在paraPkripke模型中，模型检验公式的一系列问题，如<$α和<$E <$α，必须根据否定算子<$的行为来求解举几个例子：（M，s）|= t<$（α<$β）i <$（M，s）|= t<$α <$β，（M，s）|= t<$Eα i（M，s）|= tAQ（<$α），和（M，s）|= t<$（α→β）i <$（M，s）|= tαβ。3.2实现算法QCTL的模型检验问题是对给定的paraKripke结构M，状态s∈S，公式α∈L，检验（M，s）|= tα。虽然QCTL是一个次协调时态逻辑，但我们基本上可以实现这个算法的灵感来自于[16]。这一点在最后一节中得到了证明。在深入分析图2中给出的算法之前，我们现在提供前面提到的集合Facts（α）的更准确的解释，其中α∈L，这对于构造算法至关重要。对于子句α∈L，令文字（α）={l|l是α }的析取式。 以下定义规范F acts（α）在完全子句α的情况下。定义3.2.1设α是一个完备子句。F acts（α）归纳定义如下：Sn• 如果α = 11... 如果n ≥ 1，则事实s（α）={l1 <$. 阿夫拉尔岛|Literals（l1）. （i）i=1Literals（α）}。• 如果α = σx（β1 ≤. ... . β J）|对1 ≤ i ≤ n，βJ∈ Facts（pi）}.1ni• 如果α=σ（（β 1）），. . n）U（γ1π. . . <$γm）），则Facts（α）={σ（（βJ<$. . . <$βJ）U（γJ<$. . .（J））|对于1≤1i≤n且1≤j≤m，βJ∈ Facts（βi），γJ∈ Facts（γj）}.n1mI j• 如果α=l 1 π。 . . 你好。 . . 当i≤j≤n时，qlj是一个整数，且i>1，当1≤j≤i−1时，Snlj是文字，则事实s（α）={γ1∈. . γm|对于1≤l≤m，若γl是拟文字，则γl∈m=1F acts（qli）. . n= 1，n= 1≤1，则返回CheckS（αi）i=1其他开关（α）情况α = l1π.. . 返回{s} |TestClause（s，α）= True}（m ≥ 1且对于1 ≤ i ≤ m，li是文字。）case α = cql1.. . SQLm：return CheckS（c）返回CheckS（ql1）- 是的 . . 其中，当1≤i≤m时，qli是一个qu单线性系统，且c这是一个条款。）caseα=E：r et urn{s∈S|R（s）CheckS（）=/}caseα =E（βU）：return CheckSEU（β，）caseα =EQ：return CheckSEG（）caseα =<$（β<$）：returnCheckS（<$β< $）caseα =<$E <$β：returnCheckS（AQβ）..结束开关端图三.强可满足性但是，其中，遍历以不同的方式进行，并且α的子公式集合包含由不同方式生成的公式。设Sub（α）和Subs（α）分别表示α在Check（α）和CheckS（α）中的子公式集。为了简单起见，我们没有明确给出Sub（α）和Subs（α）的全部定义，而只是表述了以下要点：• 对于p∈ P，Sub（<$p）= Subs（<$p）={<$p}，而Sub（<$p）={<$p，p}不是这种情况。具体地，对于子句c，Subs（c）={c}。这一项明确了可能由解析树的叶节点表示的子公式。• Sub（α<$β）={α<$β}<$Sub（α）<$Sub（β），Subs（α<$β）={α<$β}<$Subs（α）<$Subs（β）。对于完整子句α = c<$ql1<$. <$qln for n≥ 1，其中c是子句，且对于1 ≤i≤n，qli是拟文字，Subs（α）={c，α}<$Subs（ql1）<$. Subs（qln）.• 对于任何公式α，Sub（<$α）不能通过Sub（<$α）={<$α}<$ Sub（α）计算。我们应该根据德摩根定律，双重否定消除来计算Sub（<$α）。一些示例是按顺序的：Sub（α）=Sub（α）;特别地，当否定运算符直接作用于路径限定符E或A时，诸如<$E <$α和<$A <$α，我们应该根据相应公式的语义计算这些公式的子公式的集合。 例如，Sub（<$E<$α）= Sub（A<$（<$α）），Sub（<$A <$α）= Sub（EQ（<$α））。图2表明，当α是一个完全CNF或一个完全子句时，总是调用CheckS（α），因此，我们不关心上述情况，D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）2335子s（α）。• 对于以泛量化器A、EQα和E（αUβ）开始的这些公式，由于paraKripke模型的概念，子公式集的计算表现得很奇怪。通常，考虑E（αU）作为例子。图2显示Check（E（αU））基本上涉及对于fs∈F acSt（α），fs的变换也是fs的变换由CheckS（fs）执行。 因此，Sub（E（αU<$））={E（αU<$）}<$fs∈Facts（α）Subs（fs）<$因此，Sub（EQα）={E Qα}<$S分段（f）.f s ∈Fact s（α）sS因此，QCTL上的模型检验递归算法遍历公式α的while分析树，可以通过应用这些规则来构造以类似的方式计算Sub（·）和Subs（·），其中·表示一些公式。这个解析树的根节点表示α，而叶子节点表示节点表示原子公式、它们的否定或某些子句。构造公式的解析树的过程体现了图2和图3中的递归算法的骨架。对于p∈P，Sat（p）或Sat（<$p）的计算是直接的。为了简单起见，我们只说明当α=E（βU）时Sat（α）的计算其次，具体调用函数CheckEU（见图2），它执行Sat（α）的计算。直观地说，CheckEU的工作原理如下。显然，对于s∈ Check（α），s ∈ Sat（α），即（M，s）|= tα。 因此，Sat（α）中的所有状态最初都是被认为是属于检查（检查）。 对每个fs∈F acts（β），一个迭代过程运行，该过程计算状态空间，其中对于每个状态s，存在状态序列（s0，s1，.，s n），对于n≥ 1，满足s0= s，s n∈ Check（n），对于0 ≤ i ≤ n − 1，s i+1∈ R（s i）（集合R（s i）表示S1的直接后继状态的集合，即， R（s i）={sJ∈ S|（s i，sJ）∈R）}）和si∈CheckS（fs）. Sat（·）的计算，其中·表示这样的具有通用量化器的公式，可以近似地执行如下操作：Sat（E（βU））。CheckS（α）返回表示为Sats（α）的状态集，其中α是强满足的，如图3所示。考虑到计算Sats（α）的例程与计算Sat（α）的例程总体上接近，因此我们不对用于检查强满足性的算法进行明确的解释。4例如在这一节中，我们给出了一个简化电话系统的例子，展示了我们提出基于仿协逻辑的模型检测技术的动机。电话系统可以从不同的视角来考虑。图4（a）和图4（b）示出了电话系统上被呼叫者1和被呼叫者2的视点的两个不同的视图这两个模型使用基于二值逻辑的标准Kripke结构来指定。国家名称和国家中的命题所表达的意义可以从字面上理解。我们可以36D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）23connectedOFFHOOK=TCONNECTED=T拨号音摘机=T振铃连接=F摘机=F连接=T空闲摘机=F连接=F（一）连接+离线+呼叫器选择+CONNECTED拨号音振铃+摘机-摘机- 呼叫者选择+所有者选择- 连接±连接（c）第（1）款空闲- 摘机- 来电者选择connectedOFFHOOK=TCALLER SEL=TCONNECTED=T拨号音振铃OFFHOOK=T OFFHOOK=F CallerSEL=F Caller SEL=T CONNECTED=F连接=F（b）第（1）款空闲摘机=F呼叫器选择=F连接=F图四、（a）被访者的观点1;（b）被访者的观点2;（c）两个观点的合并很容易发现不一致发生在被调用方1和被调用方2之间。被叫方1认为电话允许在来电期间更换接收器而不会断开连接，但被叫方2认为更换接收器总是导致断开呼叫。在指定了目标系统的模型之后，即使是部分的和不一致的，我们也希望深入分析这些模型。当然，我们可以分别对这些模型进行推理，但更有趣的是，我们可以整合这两个模型（即使它们不一致），以执行对包含电话系统更全面信息的合并模型的推理。当模型之间存在不一致的信息时，集成多个模型是复杂的。我们在这里这样做：• 为合并模型选择基础逻辑QCTL。• 选择签名映射，它规定了合并模型和相应源模型之间的项的关系，例如状态的名称和状态中的命题变量。我们在[17]中采用了类似的原则。• 选择处理模型间不一致性的措施。乐观地说，我们认为，一些有争议的观点对系统并不排斥对方，例如，每个模型不否认存在的过渡，它没有描述。我们认为，这个论点适合于不断发展的规范，特别是在发展的早期阶段。图4（c）显示了产生的paraKripke模型。尽管对系统的观点有争议，但我们可以验证电话系统的一些时间属性。代表性的例子包括：1. AQ（CONNECTED→E（<$OFFHOOK））2. AQ（<$CALLER SEL→ <$CONNECTED）“如果没有选择，则无法连接。”3. AQ（<$OFFHOOK→<$CONNECTED）根据定义3.1.1，我们可以很容易地确保第一个属性在合并模型中是满意的，即图4（c）是一个paraKripke模型，D. 陈，J.Wu/Electronic Notes in Theoretical Computer Science 157（2006）2337第一个财产。其余三个属性更有趣。第二个属性在callee1中是不可表达的，但是callee1可以拥有这个属性，只要它接受callee2中对CALLER SEL的定义，而callee1没有描述。考虑第三个，从图4（c）中，我们知道合并模型满足该属性。就在这个属性上是callee1和callee2连接。请注意，列出的属性是简单的，因此，我们不明确解释从图4（c）中导出三个属性的细节。虽然上面提到的这个例子很小，而且是人为的，但它足以说明不一致情况下的推理类型5总结发言本文提出了一种基于QCTL的paraKripke模型的概念深入研究了在QCTL中判断一个paraKripke结构是否为公式的paraKripke模型在此基础上，给出了QCTL模型检测算法的实现.然而，这是一项不充分的工作。我们需要继续朝着以下方向开展工作。首先，我们打算进行一系列的非平凡的案例研究，表明所提出的框架，使开发人员更有效，更创新的不断发展的开发过程中，如需求工程。此外，我们的目标不是要取代现有的方法来处理存在于软件开发的生命周期中的不一致。我们计划将基于次协调逻辑的自动化工具与Hunter，Finkelstein等人的早期工作相引用[1] E. Clarke，O. Grumberg和D.佩尔德。 模型检查。MIT Press，1999.[2] G. J. Holzmann。模型检查器SPIN。IEEE软件工程学报，23（5）：279，1997。[3] R. K. Brayton，G.D. H