Event-B CSP的有界重传协议: 一个逐步细化的案例研究

ǁǁ可在www.sciencedirect.com在线获取理论计算机科学电子笔记280（2011）69-80www.elsevier.com/locate/entcsEvent-B CSP中的有界重传：一个案例研究史蒂夫·施耐德1 Helen Treharne2英国萨里吉尔福德大学计算机系Heike Wehrheim3德国帕德博恩大学信息学院摘要Event-B CSP是Event-B和CSP的组合，其中CSP控制器与Event-B机器结合使用，以允许更显式的方法来控制流。最近的结果提供了逐步完善此类组合的方法。本文提出了一个简化的有界重传协议的案例研究，启发Abrial的处理这个例子，说明几个方面的新的方法。案例研究包括细化步骤，以说明该细化方法的四个不同方面：（1）拆分事件;（2）引入收敛循环行为;（3）关系预期事件、汇聚事件和转移事件之间的关系;（4）汇聚预期事件。关键词：事件B，CSP，有界重传协议，逐步细化1引言本文介绍了一个案例研究，说明了CSP [7]和Event-B [6，1]组合中的细化链。该案例研究的灵感来自于Abrial该方法建立在事件B方法的基础上，逐步细化，在每个阶段引入额外 新事件需要仔细介绍，与以前的事件联系起来，并控制它们何时发生。我们的方法使用CSP而不是Event-B中的控制变量，以显式和可见的方式管理事件的控制流程1电子邮件：s. surrey.ac.uk2电子邮件：h. surrey.ac.uk3电子邮件：wehrheim@mail.uni-paderborn.de1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.01970S. Schneider et al. /Electronic Notes in Theoretical Computer Science 280（2011）69在事件B中，每个阶段都有证明义务来确定细化的有效性。CSP的引入允许在CSP框架内处理一些举证责任。特别是，与控制权转移有关的义务可以通过细化检查更容易地履行。现在，为模型建立迹线细化和发散自由等属性可以实现一定程度的自动化。这种方法的技术细节在[9，8]中给出。本文的目的是说明现在支持的细化步骤，并提供该方法的示例2CSP背景CSP是一个进程代数，它用通信组件来描述系统，并特别关注它们之间的交互。组件由进程组成，进程执行事件模式，并通过同步事件进行通信CSP提供了一种描述进程的语言。STOP是不能执行任何事件的进程。RUN（A）可以执行事件集合A中的任何事件序列。prefix进程a→P最初准备执行事件a，其后续行为是进程P的行为。外部选择PQQ是一种选择在进程P和进程Q之间。平行组合PQ是P和Q的平行组合：它们在它们共有的事件上同步，并且可以独立地执行其他事件。交错组合P|||Q是P和Q的并行组合，它们独立执行，并且不同步任何事件。抽象进程P\A的行为与P类似，只是A中的事件被隐藏了：它们在内部执行，不再位于P的接口中。最后，从一组事件到另一组事件的映射f可以用来重命名字母表：f（P）是P的字母表重命名，由此f（P）可以执行f（a），只要P可以执行a;类似地，f−1（P）可以执行a，只要P可以执行f（a）。CSP还提供了各种语义模型。在本文中，我们主要关注的是跟踪模型，它将每个进程与一组跟踪（事件序列）相关联，这些跟踪可以在某些执行过程中执行。一个过程P的所有可能迹的集合记为迹（P）。如果过程Q的任何迹也是过程P的一个迹，则过程P被过程Q限定为迹。 这是写P±TQ。在本文中，我们也关注分歧。如果一个过程在某个时刻可以执行无限序列的内部事件，那么它就是发散的我们的目标通常是建立过程不发散，并将利用结果来建立发散自由。CSP有模型检查工具，如FDR [3]和ProB [5]。这些允许对细化要求P±TQ进行自动检查，还允许对CSP过程进行无发散检查以及其他检查。本文中的所有CSP证明义务都可以使用FDR进行检查。CSP及其语义的更全面解释可以在[7]中找到S. Schneider et al. /Electronic Notes in Theoretical Computer Science 280（2011）69713Event-B的精化原则Event-B [1]根据具有状态的机器以及更新状态的事件来建模系统。机器之间的细化涉及现有事件的数据细化，也可以引入新事件。在事件B中，当新事件Ni+1被引入到Mi+1中时，它们可以被分配“收敛”或“预期”的状态此外，对Mi中的事件进行细化的事件也可以被赋予在Mi+1中收敛或预期的状态。定义为收敛事件或没有状态的事件的事件不被赋予状态。由事件状态产生的证明义务是，收敛事件必须减少M i+1的变量;预期事件不得增加它。当标准事件B数据细化证明义务在M i和M i +1之间时，我们将写为M i“ M i +1 ，收敛和预期事件的证明义务也是 如此。在Event-B机器CSP中，我们处理由非发散CSP进程Pi和Event-B机器Mi组成的受控组件，它们在公共事件上同步这种组合的语义基础在[8]中给出。一个改进步骤引入了一个新的非发散过程P i+1，使得P i±TP i+1，以及一个新的机器M i+1，使得M i“M i +1。 M i+1事件的出现有两个原因之一：(i) 它们可能是Mi事件的细化，具有相同的名称或不同的名称（这包括在每个层次中完全相同的事件）。细化事件产生映射fi+1，映射Mi+1我的事件。映射是从事件定义的精化子句中获得的，其中Mi+1中的a精化Mi中的fi+1（a）。请注意，事件B在最一般的情况下允许Mi+1中的一个事件精化Mi中的几个事件，但在这里我们允许一个事件最多精化一个其他事件。(ii) 它们可能是新的事件，并不细化Mi中的任何事件。M i+1的新事件将由N i+1表示。我们将Abrial的方法扩展到使用收敛和预期状态 通过引入一个额外的状态：“移交”。此外，为了支持关于发散自由的推理（即当新事件被隐藏时，系统不会发散），我们将要求所有新引入的事件都被赋予一个状态，所有预期事件的细化都被赋予一个状态。 一个转移的事件与预期事件类似地处理，但是在事件-边界CSP的上下文中，确保其收敛的责任被转移到CSP控制器P i+1，而不是像预期事件那样延迟到某个未来的细化步骤。因此，与细化预期事件的事件相比，细化转移事件的事件将不会被分配状态。因此，在Mi+1中，唯一具有某种状态（收敛的、预期的或已转移的）的事件是新引入的事件Ni+1和那些细化了Mi图1显示了我们将在案例研究中使用的各种细化级别的事件，还显示了映射fi收敛事件、预期事件和转移事件分别标记为（c）、（a）和（d）72S. Schneider et al. /Electronic Notes in Theoretical Computer Science 280（2011）69一期+1一期+1Fig. 1. 通过开发为了确立细化关系，必须解除几项证明义务：(i) 我们要求MiMi +1。(ii) 我们需要f −1（P i）|||RUN（N i+1）±TP i+1。 如果N i+1= N，则这等价于f−1（P i）±TP i+1，也等价于P i±Tf i+1（P i+1）。从[9]的定理5.4可以得出，P0M0至PnMn在每一级履行这两项义务时，建立了以下关系：（P0<$M0）±Tf（（Pn<$Mn）\N）S. Schneider et al. /Electronic Notes in Theoretical Computer Science 280（2011）6973SND进展当s st=工作然后sst：∈{success，端失败}BRP当s st/=工作然后r st/=工作skip端RCV进展当r st=工作然后rst：∈{success，端失败}P0=S0<$R0S0=SND进度→brp→STOP R0=RCV进度→brp→STOP图二、级别0：机器M0事件和控制过程P0其 中 f = f n;. ; f1是 事件 重 命名 的 合成 ， 并且 N = N n<$fn−1 （ Nn−1 ） <$. 。 .（fn;. . . ;f2）−1（N1）是在精化步骤中引入的所有新even的集合，适当地重命名。为了获得发散自由，我们使用第三个证明义务，以确定CSP控制器不允许转移事件发散：(iii) 衍生事件（如预期事件）不得增加变量。关于转移事件（与预期事件不同）的额外证明义务是，如果Di+1是Mi+1中所有转移事件的集合，则Pi+1\Di+1必须是无分歧的。从[9]的推论5.18可以得出，如果Mn不包含预期事件，则组合（Pn<$Mn）\N是无发散的。4有界重传协议本案例研究通过在不可靠的介质上发送数据包来说明文件的传输。CSP用于描述发送方（重复传输，并通过文件进行）和接收方（数据包的渐进接收）的重复行为，而模型的Event-B部分侧重于状态。为了这个案例研究的目的，我们只关注传输介质的不可靠性，允许可靠的确认。0级在图2所示的初始级别中，我们看到CSP控制器被拆分为发送方控制器和接收方控制器。我们从Abrial的模型开始，有一个发送者和一个接收者事件。事件brp发生在协议完成之后。74S. Schneider et al. /Electronic Notes in Theoretical Computer Science 280（2011）69P1=S1<$R1S1=（SND成功→brp→STOP）Q（SND失败→brp→STOP）R1=（RCV成功→brp→STOP）Q（RCV失败→brp→STOP）SND成功雷菲讷SND进展当s st=工作r st=成功然后s st：=成功端SND失效雷菲讷SND进展当s st=工作然后s st：=失败端RCV成功雷菲讷RCV进展当r st=工作然后r st：=成功端RCV故障雷菲讷RCV进展当r st=工作s st=故障然后r st：=失败端不变式：I1：s st=successrst=success图三. 级别1：机器M1事件和控制过程P11级在第一个细化步骤中，进度事件被分为成功和失败事件，并引入了对发送者和接收者最终状态之间关系的额外要求图3中给出了最终的机器和控制器。关联的重命名函数是f1（SND成功）=f1（SND失败）=SND进度f1（RCV成功）=f1（RCV失败）=RCV进度f1（brp）=brp此级别没有新事件。P0±Tf1（P1）。同样，M1的每个事件a都有a的精化f1（a）。因此P0M0±Tf1（P1M1）S. Schneider et al. /Electronic Notes in Theoretical Computer Science 280（2011）6975P2=S2R2S2=S1R2=RCV rcv电流数据→R2QRCV成功→brp →停止QRCV故障→brp →停止RCV RCV 当前数据地位收敛当r st=工作r+1n<然后r：=r+1g：=g<${r+1<$→p（r+ 1）}端RCV成功当r st=工作r+1=n然后r st：=成功r：=r+1g：=g<${r+1<$→p（n）}端变量：V2：n−r图四、级别2：机器M2新的和改变的事件，和控制过程P22级在第二个细化步骤中，我们引入数据文件p：1。n→D被转移。数据包的接收将在描述的接收器部分中使用新的收敛事件建模，并调整RCV成功，所有其他事件保持不变。在CSP控制器中引入了一个回路注意，在这种情况下，正是B事件的收敛确保了新事件不会无限地发生。N2是在这个级别上新引入的事件集合。只有一个这样的事件：N2={RCV接收当前数据}没有发生事件重命名，所以f2将是标识函数，可以忽略。事实上，这将是所有后续细化级别的情况图4中给出了M2引入的新事件，以及从M1和M2加强的事件，以及控制过程P2。然后是P1|||运行（N2）±TP2。因此（P1<$M1）|||运行（N2）±T（P2×M2）。3级在第三个细化步骤中，我们使用受控组件中事件的新状态：“已移交”。我们将新的事件引入发送方控制器：一个转移事件，一个收敛事件和一个预期事件。我们还将两个76S. Schneider et al. /Electronic Notes in Theoretical Computer Science 280（2011）69RCV成功当r st=工作r+1=nR=s然后r st：=成功r：=r+1端g：=g<${r+1<$→d}不变量：J3：g =（1.. r）Dp变体：V3：（n-s）g：=g<${r+1<$→d}端RCV RCV 当前数据当r st=工作r+1n

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