基于选择性μ演算的CCS规范语言验证多线程Java程序的模型检查方法

--理论计算机科学电子笔记110（2004）55-74www.elsevier.com/locate/entcs基于简化模型Sara Gradara，Antonella Santone，Maria Luisa Villani1RCOST -意大利Gigliola Vaglini2意大利比萨大学信息工程学院摘要Java主要用于开发分布式和并发系统，但测试多线程系统不能保证软件的质量;相反，验证技术给了我们更高的系统置信度，其中，模型检查方法自动建立复杂系统的属性。这些技术通常应用于规范语言，并且存在几种环境来验证并发规范的时间属性。在本文中，我们提出了一种尝试，应用模型检查技术验证多线程Java程序的一个子集。 特别是，我们使用基于选择性μ演算逻辑的工具来检查通过CCS规范语言描述的系统。保留字：状态爆炸、模型检验、CCS、Java。1介绍并发系统正变得越来越有趣，但这样的系统通常是相当复杂的。此外，由于现代计算应用程序需要高度可靠的软件系统，因此测试无法确保足够的可靠性水平。1电子邮件：gradara，santone，unisannio.it2电子邮件：g. iet.unipi.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.06.01056S. Gradara等人理论计算机科学电子笔记110（2004）55正确性形式验证技术是一个更好的选择，特别是，模型检查对于自动建立复杂系统的属性是有用的。验证技术通常应用于并发规范语言，如通信系统演算（CCS）[32]和时间排序规范语言（LOTOS）[9]，由于它们的语义简单。在此上下文中存在一些完整的模型检查环境，例如，请参见Concurrency新世纪（以下简称CWB-NC）[15]，它对表示为μ演算公式的时间属性进行验证[35]。在本文中，我们考虑到几个问题的边界使用模型检测技术。第一个问题是系统规范和代表最终产品的代码之间缺乏正式的联系因此，如果我们首先正式指定系统行为，我们可以验证此规范上属性但是，以某种方式导出相应的程序，我们不能保证它的正确性。另一个问题是，用于表示并发系统行为的模型，例如转换系统，由于通过交错表示并发性而引起状态爆炸问题;这个问题限制了模型检查技术对复杂系统的有效使用。最后，除了系统需求之外，在应用验证技术时，系统需求也必须以形式化的方式表达：这对于普通开发人员来说通常很难。在本文中，我们提出了一种尝试，应用模型检查技术验证多线程Java程序的一个子集。特别是，我们使用的工具基于：• 通信系统演算（CCS）[32]，这是一种广泛用于并发和分布式系统的专用语言;• 时序逻辑称为选择μ演算（见[5，6，7]），用于描述系统需求。这样的逻辑允许我们根据要验证的公式自动减少CCS规范，从而获得一个更便宜的模型，它是系统相对于公式的抽象（属性驱动的抽象也用于[8，10，16]，即使不是语法推导）。虽然与μ演算具有同等的表达性，但选择逻辑提供了一种更简洁和直观的方式来表达属性，因此陈述系统需求将更容易;以及• CWB-NC工具：由于选择公式可以自动转换为μ演算公式，因此可以使用CWB-NC工具包进行模型检查。为了应用上述工具，我们定义了一个Java到CCS的转换S. Gradara等人理论计算机科学电子笔记110（2004）5557SA − {} ∈ V∈ V一操作符.类似的方法在[11]中。 使用这种方法，结果我们得到规范和其实现之间的差距被弥合。第二节回顾了CCS的基本概念和基于选择μ演算的状态爆炸问题求解方法。在第3节中，我们描述了多线程Java程序到CCS规范的转换，而在第4节中，我们的方法在模型简化程度方面的有用性通过一个简单的同步问题来展示。最后，在第5节中给出了相关工作的考虑和比较。2背景在本节中，我们简要回顾了CCS和选择μ演算的主要概念。CCS [32]是一种广泛用于并发和分布式系统的规范语言，我们假设读者熟悉它。选择μ演算是一种表达系统行为属性的分支时态逻辑，已由作者等人引入在[6]中。2.1通信系统的微积分考虑有限个动作集合A={τ，a，a，b，. }。作用量τ∈ A称为内部作用量。可见动作的集合V被l覆盖，定义为τ。 每个动作l（l））具有互补作用l（l）。下面的语法定义了一个CCS进程。p：：= nil|X|α。p|p+p|p|p|p\L|p[f]其中α∈ A，L<$V，重标号函数f是全函数f：A → A，使得满足约束f（τ）= τ。此外，x是一个常数名：ea chcon stx由常数定义xd=efp定义，其中ep为称为X的身体。一个进程p的操作语义是一个标记的转移系统，（p），即，一种自动机，其状态对应于进程（初始状态对应于p），其弧由并且对应从一个状态到另一个状态的转换。这样的结构化操作语义通过表1所示的规则精确地定义。58S. Gradara等人理论计算机科学电子笔记110（2004）55p−→′p−→一∈ A动作α和α.p−→pαp+q−α→p′（andsymmetric）p−α→p′defp−α→p′Conx−α→p′x=pParp|q−α→p′|q（andsymmetric）p−→lp′，q−→lq′p−α→p′网p|q−τ→p′|q′Relp−α→p′p[f]f（α）p′[f]Resp\L−α→p′\Lα，α/∈L表1 CCS的操作语义。2.2模型检测与选择μ演算模型检查器[14]接受两个输入，一个转换系统和一个时间公式，如果系统满足公式，则返回“true”，否则返回模型检验中的主要问题是状态爆炸：事实上，系统经常被描述为具有大量状态的过渡系统。这个问题的主要原因是相互作用过程的并行组合。当n个进程的大小（状态数）m是并行组成的，所得到的过程可以是大小为mn的。在[6]中定义的选择μ演算，虽然与μ演算[35]具有相同的表达性，但在模态算子的定义上与之不同。 给定一组动作和一组变量Var，通过以下定义获得选择性μ演算公式：：：= tt|FF|Z|ϕ∨ϕ|ϕ∧ϕ|[K] R|K| VZ.|µZ.其中ZVar和K，R. 运算符µZ.和νZ.是不动点运算符：µZ.是递归方程Z =的最小不动点，而νZ.是最大不动点。在公式µZ.（νZ.）中，µZ（νZ）与Z在中的出现相结合。出现在定点运算符范围之外的变量称为自由变量。没有自由变量的公式称为封闭公式。从现在开始，我们只考虑封闭式。过渡系统的状态s满足选择性公式：S|= 0，如下所示：• s总是满足tt而从不满足ff;并且• 如果满足1.1或（和）1.2，则满足1.1和1.2（1.1和1.2）;以及• s满足[K]Rif，对于不包含S. Gradara等人理论计算机科学电子笔记110（2004）5559∪∪⟨ ⟩S我在R K中的动作，接着在K中的动作，它将进化到服从于K的状态;并且• s满足KR，如果它将在至少一个不包含R K中的动作的动作序列之后，然后是K中的动作，进化到服从k的状态。过渡系统满足条件当且仅当|其中s是它的初始状态。 CCS过程p满足，如果（p）满足，则 过程p对封闭公式的满足的精确定义在表2中给出：转移关系=I，关于IA的参数，定义如下，忽略所有不感兴趣的动作（即，（A-1）。定义2.1设p是一个CCS过程，I= A，α δα=<$I使得对于每个α∈I，p=<$qi <$p−→q，其中δ∈（A− I）<$。注意=A= −→。p|= ffp| = TTp|=|= n和p| = p|=|=P或P|=αp| = [K] RipJ. α∈K.p=KRpJ蕴涵pJ|=p| = KRJ.J. α∈K。p=αKRpJ和pJ|=p|= νZ.p| = νZn.对于所有n，p|= µZ. ip| = µZn.对于某些n，其中，对于每个n，νZn.和µZn.定义为：νZ0.=ttµZ0.=ffνZn+1.=[νZn./Z]µZn+1.=[µZn./Z]并且[X/Z]表示对于X中Z的每个自由出现的X的替换。表2一个过程对封闭公式的满足。例2.2我们给出一些选择μ演算公式的例子来解释选择算子的使用。1=[b]{a}ff：“如果a没有执行，则b不能执行“。60S. Gradara等人理论计算机科学电子笔记110（2004）55z一∧S2=3=νZ。[a]f（Z[a]{c}ff）：在此过程中，xd=efb.c.x。 +a.b.c. xyd=efa.b.c. yzd=efb. z+a.b.z图1中的过渡系统。法院认为：X|=1x |= 102x |= 103y |= 101y| = 102y| = 0.3z| = 0.01z| = 0.02z |= 103QBbFig. 1. 三个过渡制度。如[6]所示，选择性公式可以很容易地转换为利用以下定义的μ演算递归公式。[K] R = νZ。[K][A −（K <$R）] Z<$K<$R <$=µZ。K主要的一点是，与μ演算相反，选择μ演算允许我们从每个公式中立即指出转换系统中不改变公式本身真值的部分。更准确地说，检查的结果只取决于公式中使用的模态算子中明确提到的动作（即发生动作）。 例如，考虑过程p=b.c.a.nil，并假设我们我想验证属性任何行动”。 该属性可以使用μ演算逻辑表示为：= µZ。⟨a⟩ tt ∨ ⟨b,c⟩ Z使用选择性μ演算逻辑，上述性质可以等价地表示为：sel=很容易看出，该性质在S（p）上成立（见图2（a））。请注意，同样的性质也适用于一个更小的过渡系统，如图2（b）所示，这两个系统在公式方面是等价的。这样的系统可以从（p）中得到，只保留由动作a标记的转移，并因此折叠状态。因此，给定一个公式，问题是找到正确的一组动作，XB一CBCyaBS. Gradara等人理论计算机科学电子笔记110（2004）5561›−→一一(a)（b）第（1）款图二.过渡系统。改变公式的真值。现在，μ演算公式并不总是适合于识别这些动作。 例如，公式中出现的动作集合是{a，b，c}，而只有a，它单独出现在公式中，是一个保持公式真值的相关动作在[6]中，ρ-等价被定义为形式化地表征“关于一组ρ作用的相同行为”的概念因此，通过从S（p）中消除不在ρ中的动作，可以改进过程p的模型检验。显然，约化程度主要取决于ρ相对于A的大小。例2.3回想例2.2的公式和图1中的过渡系统。 S（x）是{a，b}-等价于S（z），相反S（y）不是{a，b}-等价于S（z）。因此，S（x）和S（z）对于检验在{a，b}中发生作用的公式给出了相同的结果;特别地，它们满足π2，而不满足π1。注意，发生的动作的集合是{a，b}，而发生的动作的集合是{b}，它是{a，b}的子集。Q在[5]中，CCS过程p被变换成另一个过程q，在该过程q上，选择公式可以等价地检验3。该方法基于一组形式为p q的语法转换规则;这些规则在表3中定义，由一个动作删除规则和两个压缩规则组成规则第一个删除（如果可能的话）不属于给定集合p的动作，其中包括p的发生动作;动作必须不是选择运算符在并行复合作用域中的第一个动作（这个条件需要保持ρ-等价）。另外两条规则通过消除冗余的选择分支来压缩流程。一种算法[3]在[7]中为LOTOS过程定义了类似的方法pbC62S. Gradara等人理论计算机科学电子笔记110（2004）55−→/∈动作删除规则：α.p p，如果α p和α不是并行组合紧规则：C1：α.p+p−→α.p，如果α/∈ρC2：α.p+β.p−→α.p，如果α，β/∈ρ表3变换规则。被定义为通过反复应用变换规则来减少p，直到这是不可能的。一个原型工具实现了这样的算法，而另一个工具则将选择性公式转换为μ演算公式。这些工具已集成到一个名为CCS Reduction Tool的系统中（见图3），其输出采用CWB-NC环境的格式，因此该环境可用于构建简化CCS规范的过渡系统建模，并用于检查其上的选择公式。3Java程序作者已经在并发系统的设计阶段应用了上一节中提出的方法（例如，参见[30]）。从那里获得的积极结果来看，我们认为相同的方法在多线程程序验证的上下文中可能是有用的，通过将它们翻译成现有模型检查器的规范语言，即，CWB-NC刀具这是一个更具挑战性的领域，因为真实的程序通常很大，并且它们对有限状态模型的抽象可能仍然难以通过来自状态爆炸问题的模型检查技术来处理。我们认为，应在这方面努力整合减排解决办法。我们的想法如图3所示。用于抽象Java程序的工具，应用数据或基于公式的抽象技术，如切片（参见Bandera [16]），为我们提供了一个合理的起点，以转换为CCS规范。为此，我们定义了一个Java-to-CCS转换操作符，如3.1节所述。类似的方法在[ 11 ]中提出：然而，我们的方法似乎更系统化，翻译规则是模块化的，并且从自动执行的角度考虑。遵循同样的思想，其他编程语言的transform运算符可以很容易地定义。S. Gradara等人理论计算机科学电子笔记110（2004）5563然后，我们的CCS缩减工具会对生成的CCS流程进行分析，该工具会自动删除与要检查的公式无关的所有操作。 主要优点是我们的工具可以与，而不是取代，开发了其他技术来解决状态爆炸问题，包括去除不必要的过渡交错的偏序方法[ 21，36 ]，忽略一些状态信息的抽象技术[ 13 ]，组合推理[1，12，33]和基于启发式搜索的方法[20，34]。事实上，一旦我们有了对应于初始Java程序的CCS规范，我们就可以应用上述方法。图三. 工具。3.1将Java程序转换为CCS进程读者可以参考[27]以获得有关基本Java结构的详细信息。在这里，我们解释这些结构的语义，通过他们的翻译到CCS的过程。该方法基于以下两个假设：• 程序中对象的数量是静态定义的;• 每一组变量值都是有限的。这可以通过合适的抽象方案来实现，例如数据抽象[16，19]或谓词抽象[2，17]。抽象技术必须应用于使模型检查可行，因为大多数软件程序具有无限数量的状态。在本文中，我们集中在布尔数据抽象，这已被证明是仍然相当有效的，在这种情况下。64S. Gradara等人理论计算机科学电子笔记110（2004）55不作为第一个假设的结果，一个类的（非静态）状态变量和方法被复制到每个对象，并被奇异地转换为CCS过程。第二个约束是确保变量和使用它们的方法所有的对象、变量和方法都有一个索引。也就是说，• V是变量的索引集;以及• O是对象和方法的索引集。变量包括传递给方法或在方法中使用的对象状态变量和局部变量。我们已经形式化的同步方法和Java特性，如对象锁和等待集，与它们引用的对象具有相同的标识符。我们在CCS代数中添加了以下运算符来表示两个进程的执行顺序。定 义 3.1[ 序 列 算 子 ;] 设 p 和 q 是 两 个 CCS 过 程 。 该 方 程 定 义 为 ：p;qd=efp{q/nil}，用过程q替换p中以及所有包含常数的主体中出现的nil。在本节剩余部分中定义的运算符适用于程序的Java代码，将其转换为CCS规范。由于篇幅有限，本文只给出T的一部分定义，特别是理解我们的方法在第4节所述例子中的应用所需要的内容。关于T的定义的更多细节见[22]。3.2变量和方法过程与每个变量和方法对应的过程定义见表4。最佳变量定义。每一次，布尔变量VAR i可以被视为与其当前值相对应的进程。我们相应地定义了两个过程，VARffi和VARtti。例如，分支是F alsei。VARffi表示变量的false状态;在执行操作setT ruei之后，该状态将变为true，并且该过程将继续为VARtti。主要定义。方法main（）被转换为进程MAIN，其中T根据以下规则应用于I中包含的指令：S. Gradara等人理论计算机科学电子笔记110（2004）5565def我我我我1我2T（boolean V ARi）= V ARffi= isFalsei.V ARffi+ setFalsei.V ARffi+ setTruei.VARttiVARttd=efis T rue. VARtt+set T rue. VARtt+set Fa lse. VARffI I I I I I IdefT（main（） {I}）=M AIN=T（I）defT（methodNamei（）{I}）= MET HODN AMEi= callMethodNamei。T（I）returnMethodNamei.M ET HODN AM EiT（run（）{I}）=Rund=effallRun. T（I）表4变量和方法的定义。表5.方法定义。每个方法都对应于一个等待通过操作callMethodNamei调用的进程。操作返回方法名称为导致控件返回到方法调用方。然后，流程返回到起始操作，以便可以再次调用它。 一个特例是进程RUNi，对应于线程对象的方法runi（），只能执行一次。3.3指令表5显示了主要Java指令的翻译T（I1;I2）= T（I1）; T（I2）T（V ARi=true;）=setTruei.nilT（while（V ARi==true）I）=WHILE哪里W HILEd=ef是真的。T（I）;W HILE+为False.nil我我T（if（V ARi==true）I1;I2）=IF哪里IFd=ef是真的。T（I） +是F α1ε。T（I）T（methodi（）;）=callMethodNamei.returnMethodNamei.nilT（runi（）;）=callRuni.nilT（synchronized（this）{I}）=locki. T（I）;unlocki.nil表5说明。66S. Gradara等人理论计算机科学电子笔记110（2004）55两个JAVA指令的序列。 两个Java用操作符来表示指令;（在定义中引入）第3.1节：翻译的过程。我们假设这些指令包含在某个方法的定义中。赋值操作和“while”和“if”结构的翻译反映了它们在编程理论中的含义。特别是，它们与某些可变过程同步。一个分派行动。将真值赋给变量VAR i是由执行动作setT ruei然后终止的进程执行的。假值的赋值定义类似。WHILE构造。 WHILE过程模拟while控制控制条件，也就是说，通过动作检查V ARi的当前值isT ruei和isF alsei：取决于执行什么动作，激活或不激活与块指令IIF构造。 IF过程模拟if控制结构询问V ARi的当前值：执行块指令I1的转换或对应于I2的转换，这取决于执行的操作（分别为isT ruei或isFalsei）。方 法 呼 叫 。通 过 对 象 对 方 法 “methodName i“ 的 调 用i 由 操 作callMethodNamei 执 行 。 对 调 用 方 进 程 的 控 制 通 过 操 作returnMethodNamei返回。 相反，对于runi（）方法，控制立即返回，以允许进程的并行执行。JAVA同步块或方法。 在翻译我之前，对象i必须通过动作locki获取;动作unlocki遵循I的转换以释放锁（参见表6）。3.4并发构造和方法表6显示了Java构造和方法的并发转换。也就是说，进程WAIT描述了监视器的概念，进程WAIT和NOTIFY对应于wait（）和notify（）方法，进程WAITSET代表与任何对象相关的等待集管理为了表示这些构造，对Java语言规范进行了仔细的好的。 此过程模拟对象的S. Gradara等人理论计算机科学电子笔记110（2004）5567我我我我我我I I I I I III I I I I I II−我我我我我我LOCKd=eflOCK. 锁上了。LOCKWAITd=有效W AIT。因瑟河联合王国是你。lock。你知道吗？WAITNOTIF Yd=有效NOTIFY。（我也是。resume。remove. 我不知道。N OTIF Y+noneInqueuei.returnNotifyi.NOT IFYi）WAITSET（0）d=efinse rt. WAITSET（1）+noneInQueuei.W AIT SET（0）i设j为0

下载后可阅读完整内容，剩余1页未读，立即下载