替换精化证明B中可达性的方法

⇒⇒可在www.sciencedirect.com在线获取理论计算机科学电子笔记280（2011）47-56www.elsevier.com/locate/entcs使用替换精化证明B中的可达性Marc Frappiera，1，2 Fama Diagnea，b，3 Amel Mammarb，4一个GRIL，D'ep。b巴黎南部电信研究所，法国巴黎摘要本文提出了一种利用经典B中的替换精化来证明形式AG（EEF φ）的可达性的方法. 这样的性质表示对于满足φ的每个状态都存在一条到满足φ的状态的执行路径。这些属性经常出现在安全策略和信息系统中。我们展示了如何使用Morgan的规范语句来表示一个属性，并使用精化法则来证明它，其思想是通过逐步精化来构造一个程序，该因此，这种程序的执行提供满足AG（ΔEF φ）的执行。证明义务使用断言（B的ASSERTIONS子句）来表示，并且可以使用Atelier B来履行关键词：B记法，证明，可达性，CTL，精化演算1引言可达性属性经常出现在信息系统和安全策略中。例如，在图书馆系统中，一个典型的属性是成员应该总是能够借阅一本书。如果有书可借，而会员还未达到借阅限额，会员可以立即进行借阅;如果达到借阅限额，会员可以归还一本所借图书，然后再借阅。 如果这本书已经被另一个成员借走了，那么他可以 他预订了房间，等着轮到他借书。在这个描述中，我们看到，在证明这样一个性质时，指定者必须考虑几种情况它们在需求分析期间记录在用例和场景中1本研究部分由加拿大自然科学和工程研究委员会（NSERC）支持。2电子邮件：Marc. USherbrooke.ca3电子邮件：Fama. USherbrooke.ca4电子邮件：Amel. it-sudparis.eu1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.01748M. Frappier et al. /Electronic Notes in Theoretical Computer Science 280（2011）47在临床信息系统中，出现类似的属性，特别是当使用访问控制规则和患者同意规则时。人们希望确保在紧急情况下，医生仍然可以获得期望的信息，或者适当地处理科室之间的患者转移等。这样的可达性属性可以用CTL [8]表示，因为只需要显示路径的存在。LTL [18]是不合适的，因为所有执行路径都必须满足LTL属性。我们的可达性属性不需要所有执行路径都满足：例如，成员永远不会被迫借书。事实上，这些属性在80年代初引发了CTL的定义这种形式的可达性在CTL中表示为AG（λEFφ）。该公式表示存在从满足φ的每个状态到满足φ的状态的执行路径。在证明经典B抽象机的CTL性质的上下文中，执行路径是一系列操作调用。有一种方法可以证明可达性属性是提供程序P，该程序P的基本语句是与某些运算符组合的操作调用，并且示出：[p]φ。算子这个陈述实质上是说，p，当开始于φ时，保证终止于满足φ的状态。通过证明这一陈述，人们证明了从φ到φ的路径的存在性。如果使用B替换来构造p，那么B理论可以用来证明这个陈述。像Atelier B这样的现有工具不能直接处理像[p]φ这样的表达式，但是这样的表达式可以很容易地转换为断言，使用“[ ]"定律然后可以使用Atelier B等传统工具来证明它。然而，从[p]φ生成的证明义务可能很大且复杂，因此很难证明。这就是为什么引入精化演算的想法[2，3，10，13，15，17]。在本文中，我们展示了如何在B上下文中使用Carroll Morgan [14]的有据可查的精化演算来第2章使用替换细化证明可摩根提出了一些改进规则，以逐步的方式开发顺序程序他引入了指定语句的概念，用w：[pre，post]表示，指定一个计算，当它在满足pre的状态下开始时，必须通过修改变量w在满足post的状态下终止。为了避免与“[。. . ]我们从符号中删除w，因为它满足我们的目的，隐式地让w表示B机器的所有变量注意，这个语句可以用B写成：w：[pre，post] = PREpre THEN ANYwJ WHEREpostJ THENw：=wJ（1）Spec（pre，post）的wp语义定义如下：[质量标准（前，后）] Q优惠前（前·后）M. Frappier et al. /Electronic Notes in Theoretical Computer Science 280（2011）4749ΔΔΔΔΔΔΔ2我们可以通过一个代换S来证明一个具体化陈述的精化，如下所示：质量标准（前、后）±S优惠（前[S]后）（2）因此，证明CTL可达性公式AG（λEFφ）的问题可以表述为找到一个程序S，使得Spec（λ，φ）±S。 我们将展示如何使用摩尔根在[14]中提出的精化定律来进行这些证明作为第一个例子，让我们考虑一个描述图书馆系统行为的B机器，并证明一个成员总是可以借到一本书（见附录A）。因此，我们要证明以下内容：AG（me∈memberbo∈bookEFbo <$→me∈loan）B机器变量member、book和loan分别表示图书馆的成员、图书和借阅的集合。这个CTL公式的所有变量都是隐含的普遍量化的。在续集中，我们将使用以下焦点：=me∈member因此，我们必须找到一个程序S，使得Spec（ψ，φ）±S。 我们将使用摩根定律通过逐步的算法精化（即B替换精化，而不是B机器精化）来构造S。S将遵循的执行路径可以概括为如下：i）如果会员已经达到他的借阅限额，则归还会员所借的一本书;ii）如果该书是被借的，则归还它; iii）如果该书有预订，则取消它们。这是一种路径上的蛮力策略，也可以证明对应于更可能场景的其他路径。我们将在本节结束时回到这一讨论。现在，这个蛮力策略足以证明我们的CTL公式。第一步是将规范分解为两部分：第一部分将建立一个足以满足操作Lend的前提条件的条件C1;第二部分将从C1开始并建立φ，然后我们将通过调用Lend来显示其细化。因此，我们的第一个改进步骤如下：质量标准（φ，φ）±S1;S2（3）哪里S1=Spec （ ， C1 ）S2=Spec （ C1 ， φ ）C1=C2C3C4C=Δcard（loanD{me}）MaxNb贷款C3=bo/∈dom（loan）C4=保留（bo）= []50M. Frappier et al. /Electronic Notes in Theoretical Computer Science 280（2011）47ΔΔRefinement（3）可以直接用[14]的3.3定律证明：Spec（pre，post）±Spec（pre，mid）;Spec（mid，post）（4）我们可以通过对Lend的操作调用来细化S2。S2±Lend（me，bo）（5）这个修正可以用（2）来证明。S2±Lend（me，bo）⇔（C1[Lend（me，bo）]φ）这个证明可以通过使用标准B公理重写[Lend（me，bo）]φ来解除，这导致了下面的公式，可以通过将其作为断言添加到库机器中来证明ψ∧C1 ⇒me ∈MEMBERID ∧me<$member<$bo<$BOOKID<$bo<$book<$bo/∈dom（loan）reservation（bo）=[ ]信用卡（贷款D{me}）最大NbLoans贷款bo<$<$→me∈loan+{bo<$→me}<我们现在已经通过将它细化为一个替换来求解S2，该替换的基本状态是操作调用。我们将分三步求解S1S1±S3;S4（6）S3=质量标准（μ，μC2）S4=Spec（C2，C1）我们可以用（4）再次证明（6）规范S3规定成员不应达到其贷款限额。为了解决这个问题，我们可以测试C2，这可以确保没有达到借阅限制;如果C2为假，那么我们非确定性地选择了一本成员的借阅书籍并将其归还，以建立C2。因此，S3求解如下：S3±IF <$C2然后S5结束（7）哪里S5=ΔANYboJ其中boJ∈loan−1[{me}]则返回（boJ）END（8）M. Frappier et al. /Electronic Notes in Theoretical Computer Science 280（2011）4751我们可以使用（2）和B公理证明（7）“[IF]”，产生适当的证明义务。我们可以用一个IF语句和一个循环来解决S452M. Frappier et al. /Electronic Notes in Theoretical Computer Science 280（2011）47ΔΔ∈8ΔS4±S6;S7（9）S6=质量标准（≤C2，≤C2≤C3）S7=质量标准（≤C2≤C3，≤C1）S6±IF <$C3THEN返回（bo）结束（10）S7±WHILE <$C4DOS8不变量C2C3VARIANTsize（reservation（bo））END（十一）S=ΔANYmeJWHEREmeJran（reservation（bo））THENCancel（meJ，bo）END我们可以用（4）直接证明（9）。我们可以使用（2）和“[IF]”的B公理来证明（10）（11）的WHILE语句不是B符号中语法上可接受的WHILE语句，因为它的循环体不使用实现替换，但WHILE语句的语义和规则对任何替换都有效，因此我们可以使用它们来生成证明义务。我们可以使用[14]的第5.5条证明（11），前提是我们履行以下证明义务。C2C4[S8]（* 循环体保持不变 *）C2C4[n：=V][S8]（V n<）（* 环体减少变量V=size（reservation（bo））*）<$$>C2<$C3<$$>C4<$V∈N（* 变量是自然数 *）请注意，循环的初始化没有证明义务，因为循环精化了S7，其前提条件是循环不变式。我们已经添加了我们从（5），（7），（10）和（11）手动生成的证明义务作为断言。它们在ASSERTIONS条款中附录A的库规范中提供。这些断言生成14 PO; 10个是自动证明的，4个是很容易证明的交互式证明。图1提供了通过将该细化树的叶子拼凑在一起而获得的程序。通过精化的传递性，这个程序精化了Spec（λ，φ），它本身表示CTL公式AG（λEFφ）。这个程序执行操作调用，因此它提供了一个从φ到φ的执行路径。其他解决方案可以探索更可能的情况。例如，用户可以在以下情况下进行预订：这本书是借来的;在操作TakeandReturn或Cancel上的循环将清空预订列表，并允许成员最终借阅这本书。这些替代解决方案也应该是可设计的逐步细化。3相关工作还有其他尝试实现摩根的精化演算。精化计算器[6]使用HOL来形式化精化演算并进行证明; PRT [7]使用Ergo。通过重用B工具，我们避免了形式化精化理论;相反，我们重用了B理论M. Frappier et al. /Electronic Notes in Theoretical Computer Science 280（2011）4753¬∈如果<$C2则ANYboJWHEREboJ∈loan−1[{me}]THENReturn（boJ）END END;如果<$C3则返回（bo）结束;而C4则执行ANYMEJ WHEREMEJRAN（reservation（bo））THENCancel（meJ，bo）END不变量C2C3VARIANTsize（reservation（bo））END;借（我，博）Fig. 1.该程序细化了可达性属性在一篇配套论文[12]中，我们概述了另一种证明可达性的方法。我们提出了一个算法，给定一个路径表达式，生成证明义务的AG（EAFφ）。路径表达式是在基本路径之间的一种天使般的选择。基本路径以前提条件开始，并包括操作调用或操作调用上的循环。所产生的证明义务比通过本文提出的方法获得的证明义务稍微复杂一些，但指定者不必经历逐步的细化过程。另一方面，逐步细化在构造显示路径存在的程序时提供了更大的自由。BrownandM'ery[5]已经展示了 如何使用wp演算在Atelier B中实现UNITY的Abrial和Mussat [1]为事件B的祖先引入了UNITY的leadsto模态。UNITY通过显示一组事件减少变量V来证明这种模态，非常像我们使用的while循环规则5.5 [14]。在[1]中，事件有一个守卫，通过加强它来细化它，从而潜在地消除了一些执行路径。为了确保执行路径被守卫细化所保留，还必须证明守卫的析取没有被加强。因为我们使用经典B并带有运算的前提条件，替换精化直接保持了从φ到φ的路径的存在性，所以我们没有额外的证明义务。这也意味着B抽象机的任何实现也将满足我们的可达性属性。[1]的工作在[4]中得到扩展，增加了UNITY在我们的工作中，我们不考虑公平性，因为它与信息系统（IS）无关，因为IS用户永远不会被迫调用操作。但是，我们必须考虑while循环上下文中的进度。在[20]中提出了确保和引导Pnueli等人的工作 [11，19]可能与我们的工作最接近。它包括了一些规则来证明CTL的合法性，同时也兼顾了公平和正义。他们的方法是将CTL的基本公式简化为不含时间连接符的基本公式，然后使用初等规则证明。 我们计划研究如何使这些规则适应细化环境，以便处理54M. Frappier et al. /Electronic Notes in Theoretical Computer Science 280（2011）47更复杂的CTL公式。[19]中的E-UNTIL规则是AG（λEFφ）证明所涉及的主要规则.它需要找到一个不变的V和一个变量V。我们在下面提供它，为EF实例化它。ψ→ϕ→φ <$$>wJ·ρ（w，wJ）<$$>J<$VJ

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