简化系统规格证明：一种改进的证明技术在理论计算机科学中的应用

理论计算机科学电子笔记137（2005）5-22www.elsevier.com/locate/entcs关于系统性质的更简单的推理：一种改进证明技术D.阿提亚1号，S.王2，J. C. P. 伍德考克3英国约克大学计算机科学系摘要关于系统规格的证明是很难进行的，特别是对于大规格。使用抽象和细化，我们提出了一种证明技术，简化了这些证明。我们将该技术应用于不同复杂度的Circus（Z和CSP的组合）规范。有趣的是，所有的证明都是在Z中进行的，即使是那些关于反应行为的证明。关键词：证明，完善，马戏团，Z1介绍系统形式化开发的核心是抽象规范的构建，以及将这些规范细化为更具体的设计。通常情况下，我们需要证明起始规范满足某些性质。这些可以是简单的一致性检查（例如，初始化定理）或其他一般性质（例如，并发系统中死锁/发散的自由度如果这些性质在细化步骤中得以保留，那么在初始规范中证明它们就意味着它们在后续设计中也成立。然而，这些证明往往很难进行，特别是对于大规格。1电子邮件地址：diyaa@cs.york.ac.uk2电子邮件地址：king@cs.york.ac.uk3电子邮件地址：jim@cs.york.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.0226D. Atiya等人理论计算机科学电子笔记137（2005）5本文提出了一种证明技术，便于推理系统规格。这个想法很简单：把规范看作是一个更抽象的模型的“设计”，在这个模型中，证明更容易进行。证明一个规范S满足一个性质P：(i) 提出一个更抽象的模型，比如A，S(ii) 证明P对A(iii) 证明S是A当然，证明步骤ii-iii的证明此外，这些步骤隐含地假设性质P被步骤iii中的精化关系所保持。在本文中，我们将上述改进证明技术应用于Circus[12]规格。虽然一些性质是关于一致性的，例如免于死锁，但所有的证明都是在Z中进行的。这本身就是一个有趣的结果，因为Z及其工具支持传统上仅限于顺序程序。本文的其余部分组织如下。第2节简要介绍了Circus规范语言。第3节描述了改进证明技术，并将其应用于两个不同复杂性的最后，第4节讨论了我们使用所提出的技术的经验，并得出结论。2马戏团Circus是一种统一的编程语言，它结合了Z和CSP结构，以及指定语句[9]和保护命令[6]。通过将Z和CSP集成到语言中，Circus可以用于描述并发系统的面向状态和行为方面。虽然在文献中还有其他几个结合Z和CSP的例子（例如，参见[7]中的调查），但Circus以精化理论[4，5，11]区分开来，用于以类似Morgan的计算风格从其规格中导出程序Circus有一个定义良好的语法和形式语义[12]，以及各种细化规则[5]将规范细化为设计/程序。Circus程序是一个序列：• Z段落：声明类型、全局常量和程序中定义的进程所使用的• 通道定义：声明类型化的通道，进程可以通过这些通道进行通信或同步。• 进程定义：声明封装状态和反应行为。D. Atiya等人理论计算机科学电子笔记137（2005）57在最简单的形式中，过程定义是描述内部状态的Z段序列，以及描述状态中可能的变化和/或过程与其环境之间的相互作用的操作序列。 这些操作称为操作，并根据以下方面进行定义：Z模式、CSP操作符和保护命令）。在更复杂的形式中，一个过程可以用CSP的运算符定义为其他过程的组合。2.1示例：受保护的自然数我们使用Circus来建模一个简单的过程（ProtNat），该过程封装并提供对自然数的互斥访问该过程如图1所示，可描述如下：全球定义从给定的ProcID集合中提取的其他进程通过三个通道与ProtNat交互：写入、读取和离开。写（读）通道上的通信表示进程更新（读）ProtNat中封装的数据的事件。通道leave上的通信表示进程完成了对ProtNat的当前写（读）操作。过程状态ProtNat状态中有三个组件。• 封装的数据类型为N。• 读取器集，即当前正在从ProtNat读取的进程。• 写入器集，即当前正在写入ProtNat的进程。正如ProtNatState模式所表示的，有两个状态不变量。• 阅读和写作是相互排斥的。• 不应该过程动作该过程的组成动作是(i) InitProtNatState：初始时没有读取器或写入器，被存储的数据被赋予初始值d？。(ii) 更新：只有当当前没有读者或作家时，才启用此操作。启用时，操作由8D. Atiya等人理论计算机科学电子笔记137（2005）5^[ProcID]通道读、写：ProcID×N通道离开：ProcID过程sProtNat=^开始ProtNatState数据：N读者，作家：FProcID作者/=写作者=#writers≤1InitProtNatState=^[ProtNatStateJ;d？：否|数据J=d？[阅读者J=作者J=读者]Update=^作者=读者=&写作？身份证？d：→writers：={id};数据：=dRe treieve=^wri ters= &read？id！data→readers=readers{id}WriterLeave=离开？id：writers → writers：=编辑Reader Leave=^l eav e？id：reeaders→reeaders：=reeaders\{id}React iveBehaviour=^端µX·（UpdateQQWriterLeaveQReaderLeave）;X• InitProtNatState;反应行为Fig. 1. CircusProtNat进程进程标识符和要写入的新值4.进程成为唯一的写入者，数据相应地更新(iii) ：只有在当前没有编写器时才启用此操作。启用时，通过进程标识符的输入通信和当前数据值的输出来发出动作信号。过程变成了读者。4为简单起见，我们将更新操作视为向ProtNat写入新值，而不是基于数据的当前值计算这些值。D. Atiya等人理论计算机科学电子笔记137（2005）59(iv) WriterLeave：当一个进程完成了当前的写操作，它离开ProtNat;这是通过leave通道上进程标识符的通信来通知的。(v) ReaderLeave ： 当 一个 进程 完成 了当 前的 读取 操作 ， 它将 离开ProtNat;同样，这是通过leave通道上的进程标识符的通信来通知的。(vi) ReactiveBehaviour ： 重 复 地 在 Update 、 Rewrite 、 WriterLeave 和ReaderLeave之间进行外部选择过程的外延行为由其主作用量InitProtNatState;反应行为作为对模型一致性的有用检查，我们通过证明ProtNat过程存在初始状态来结束本节。定理2.1初始ProtNatStateJ·初始ProtNatState证据每个状态组件都由InitProtNatState中的等式固定。这些等式中的表达式平凡地满足ProtNatState不变量（通过一点规则和命题演算和集合论的性质）。Q3再完善的证明为了证明一个Circus规范S满足一个性质P：(i) 定义一个抽象A，它具有与S相同的结构和状态成分，具有相同的类型和不变量。 这种抽象可以通过移除现有的保护、将外部选择更改为内部选择和/或将模式操作更改为无约束模式来获得。(ii) 证明A满足性质P。(iii) 利用Circus的精化定律证明了A±S。正如下面的例子所示，这个想法是，在步骤i中定义的抽象模型将具有非常简单的结构，步骤ii中的证明将是简单的，如果不是直接或明显的话。而且，在步骤iii中证明Circus定律的副条件应该比证明S满足P的直接猜想更容易。10D. Atiya等人理论计算机科学电子笔记137（2005）5^[ProcID]通道读、写：ProcID×N通道离开：ProcID处理AProtNat=^开始AProtNatState数据：N读者，作家：FProcID作者/=写作者=#writers≤1InitAProtNatState=^[AProtNatStateJ;d？：N]N·写。ID. D ：→BAProtNatStateAUpdate=^id：ProcID;d：N·读。ID. D →APOPROTNatStateARetrieve=^id：ProcID;d：AWriterLeave=id：ProcID·leave.id→ProtProtNatStateAReader Leave=ProcID·L eave。id→AProtNatStateAReact iveBehaviour=^端µX·（AUpdateHAWriterLeaveHAReaderLeave）;X• 初始化A ProtNatState;A Reactive Behaviour图二. CircusAProtNat流程3.1示例1：ProtNat是无死锁和无分歧的如图2所示，抽象模型AProtNat具有与ProtNat相同的结构、状态组件、类型和不变量。 抽象模型也使用相同的通道，并具有与ProtNat中定义的类似的动作。然而，在AProtNat中没有保护，并且状态变化不受约束，只要保持状态不变即可。最后，抽象模型的主要行为是在初始化状态之后，我们现在证明AProtNat是无死锁和无发散的。这意味着AProtNat的动作保持状态不变量，否则D. Atiya等人理论计算机科学电子笔记137（2005）511该过程将不是无发散的。定理3.1如果ProcID非空，则抽象AProtNat是无死锁和无发散的。证据通过对Circus语法和语义的考察，有八个条件足以使Circus进程既无死锁又无发散(i) 它是连续的。(ii) 它是免费的隐藏。(iii) 它(iv) 所有的内部和外部选择都在非空集上。(v) 它的通道类型是非空的。(vi) 其局部定义是令人满意的。(vii) 其主动作(viii) 它的行为完全是国家的条件（i）条件（iv）和（v）由定理的附带条件保证。条件（vi）是平凡满足的，因为没有局部定义。条件（vii）可以表述为你说什么？：N·InitAProtNatStateJ·InitAProtNatState扩展模式，我们必须证明，你说什么？：N·读取器数据J：N;读取器J，写入器J：FProcID·（readers J/=N=n）n#writers J≤1这是真的，因为N和ProcID都是非空的。最后，条件（viii）从总体的动作的构造中平凡地得出，但是任意的状态变化是ATProtNatState：所有动作都有真正的守卫并且永远不会中止。Q现在，如果我们可以证明ProtNat是AProtNat的改进，那么我们可以得出结论，ProtNat也是无死锁和无分歧的。此外，ProtNat的主动作也必须保持状态不变量，否则AProtNat不会是无发散的。我们在定理3.2中陈述并证明ProtNat是AProtNat的改进，这将利用以下三个定律5。[5]这些定律的证明是[2]中报告的工作的直接结果12D. Atiya等人理论计算机科学电子笔记137（2005）5第一定律是关于内部选择在一定数量的预设行为上的细化利用这一定律，内部选择可以转化为一个外部选择的一些防范行动。定律1假设，对于i∈I，ci是一个通道，Si和Ti是子集在ci上的可通信值中，Ti是非空的，Ai和Bi是动作，gi是状态上的布尔值表达式，pre是关于状态的断言然后{pre};i：I·（x：T i·c i. x→Ai）±Qi：I·gici？x：Si→Bi提供(i) prei：I·giSi/=(ii) i：I·Si(iii) Ai±Bi，对于所有i：I假设{pre}用于记录抽象操作Q法则2适用于有保护的预先固定的动作。简单地说，该定律指出，如果该动作确实与其环境进行了通信，那么守卫（g）和通信值（x）就在通信之后的那部分动作的范围内。定律2假设A是一个动作，g是A的状态的保护，c是一个通道，S是c的可通信值的子集。gc？x：S→A=gc？x：S→ {g<$x∈S}AQ法则3规定了将模式操作细化为赋值语句的必要条件。法则3假设Op是一个对状态的模式操作，变量为x和w，e是一个与x类型相同的表达式，pre是作用域中变量的断言。Op±{pre}x：= e提供了pre-pre-Op-pre-Op [xJ，wJ：=e，w]符号S [y：= f]表示谓词S，其中f系统地代替y。Q使用定律1AProtNat.D. Atiya等人理论计算机科学电子笔记137（2005）513、、、、、、理论m3.2ProcID/=ΔProtNat±Pro tNat证据从[5]，并且由于AProtNat和ProtNat具有相同的状态，如果(a) InitAProtNatState± InitProtNatState(b) A反应行为±反应行为从定理2.1可以得出但书（a）。我们还知道±通过递归分布。因此，为了证明但书（b），证明以下内容就足够了：（AUpdateH.. HAReaderLeave）±（更新Q.. QReaderLeave）反过来，这是将定律1应用于AProtNat行动的非决定性选择的直接结果。因此，我们现在所要做的就是证明（定律1的）条件1 -3对AP r ot N a t和P r ot N a t a c tion s成立。为了证明Proviso（i），并且由于ProcIDi=0，因此足以证明：p re（（wri tersreaders=）（wri ters/=）（wri ters=）（readers/=）），这是微不足道的满足，因为后件总是正确的。此外，Pro- viso（ii）是平凡满足的，因为抽象集合都是类型。根据第2号法律，但书（三）源自以下举证义务：(i) 更新[AProtNatState;id？：ProcID;d？：N]±，readers<$writers =<$id∈ProcID<$d∈N，;writers：={id};data：=d(ii) 检索[PROTNAT状态; 身份证？：ProcID]±writers=读取器ID∈ProcID ;readers：=读取器ID {id}(iii) WriterLeave[AProtNatState;id？：ProcID]±，id∈writers，;writers：=0(iv) ReaderLeave[PROTNAT状态; 身份证？：ProcID]±id∈readersf;readers：=readers\{t}14D. Atiya等人理论计算机科学电子笔记137（2005）5起重机机器人臂1臂2表进料带铺放带新闻图三. 生产单元证明义务（更新）直接来自引理A.1，在附录A中给出。 其他义务也有类似的证明。Q最后，我们现在可以实现这个例子的主要目标，并证明ProtNat进程没有死锁和分歧。理论m3.3如果ProcIDf=0，则Pro tNat是确定的，并且是潜水的。证据 这是定理3.13.2实施例2：生产细胞生产单元是一个来自工业的现实案例研究，代表了金属工厂中使用的实际安装。该系统具有中等复杂性，可以用状态数为1012的有限自动机建模[8]。如图3所示，生产单元系统包括同时工作的六台机器：进料带、升降台、机器人、压机、沉积带和起重机。从金属板材的角度来看，一般的生产是：– 进料带将金属板输送到工作台。– 工作台升高并旋转，以便机器人可以拿起盘子。– 机器人用它的第一只手臂拿起金属板，然后反转，将金属板送入压力机。– 压力机锻造钢板并返回底部位置以便卸载。D. Atiya等人理论计算机科学电子笔记137（2005）515^^BeltStatus：：=无板|端前板|端板通道开始，下降processFeedBelt=beginFeedBeltStat e=^[fb：BeltStatus]J JInitFeed BeltStat e =^[Feed BeltStat e |fb=noplat e]LoadFeedBelt=fb=无板开始→fb：[true，fbJ=板结束前]JTransferPlate=^fb=plat eboreendfb：[true，fb=plat eatend]JUnloadFeedBelt=^fb=plat eatenddrop→fb：[true，fb=noplat e]• InitFeedBeltState;µX·（LoadFeedBelt;TransferPlate;UnloadFeedBelt）;X端见图4。FeedBelt工艺– 机器人用其第二臂从压机上拾取印版，然后进一步旋转以将印版卸载到沉积带上。– 存放带将钢板输送到行车上。– 起重机从存放带上拾起金属板，移动到进料带，然后卸载金属板;新的循环开始。机器人可以回到工作台上拿起一块金属板，而压力机正在锻造另一块金属板，这一事实使这个过程更加复杂。在文献[1]中，我们给出了Circus中生产单元的形式化模型。我们还使用上述逐点验证技术来证明，所提出的模型是无发散的。由于篇幅所限，我们无法详细介绍生产单元的完整Circus模型或进行的正式证明。尽管如此，作为使用改进证明技术的另一个例子，我们在这里提出了传送带机器的Circus模型，并证明它没有死锁和发散。该过程如图4所示，可描述如下：全球定义在任何时刻，要么皮带上没有盘子，要么有盘子在皮带上，但它没有到达皮带的末端，或者有一个16D. Atiya等人理论计算机科学电子笔记137（2005）5板正好位于带6的最末端。进料带从起重机接收金属板，通过通道开始同步发出信号，并将其运输到另一端，在那里可以将其下降到升降台。过程状态进料带的状态仅用一个变量fb来描述。过程动作该过程的组成动作是(i) InitFeedBeltState： 最初，进料带不承载印版。(ii) LoadFeedBelt：只有当皮带上没有板时，此操作才启用。新印版到达传送带由通道开始时的同步事件指示。该动作的结果是相应地改变进料带的状态。(iii) TransferPlate：只有当有一个板不在进料带的最末端时，此操作才启用。该动作的效果是将该板转移到带的最末端(iv) UnloadFeedBelt：第二个动作是将板卸载到工作台上，该事件由通道下降上的通信发出信号。只有在皮带的最末端有一个板时，才能执行此操作。该动作的结果是改变状态变量以指示皮带上不再有板因此，进料带的加工顺序是：装载板，将其转移到最末端，然后将板卸载到工作台。这个序列是无限重复的。关于FeedBelt过程的一个有趣的评论是，它可以表示为顺序组合，其中顺序组合中每个动作的后置条件保证了后续动作的保护。此外，每个动作的警卫都保证了该动作的先决条件。我们将这些评论形式化为引理7，因为我们将在本文的稍后阶段需要它6为了简单起见，我们假设在任何位置上，在进料带上最多可以有一个板。时间的瞬间。即使在这种假设下，生产单元仍然可以同时处理多达5个平板。[7]在[1]中有这个引理的一个推广版本，因为类似的评论适用于我们的生产单元的CircusD. Atiya等人理论计算机科学电子笔记137（2005）5170我我我引理3.4设Main为FeedBelt过程的主动作。 然后，主可以表示为：主= A0; μX·（g1&A1;... ;gnAn）;X其中– A0=[S J|后J]– 对于所有1≤i≤n，Ai是一个（预固定的）指定语句Ai=ci→αS：[prei，postJ]– 对于所有i，prei不包含虚线变量，postJ不包含未虚线变量变量此外，以下属性适用于gi、prei和postJ(i) 吉吉|0

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