环境模型指导下的事件B形式化建模及系统开发策略

可在www.sciencedirect.com在线获取理论计算机科学电子笔记280（2011）57-68www.elsevier.com/locate/entcs环境模型指导下的控制系统开发Simon Hudon1 Thai Son Hoang2，3计算机科学瑞士苏黎世联邦理工学院（ETH-Zurich）苏黎世，瑞士摘要Event-B是一种形式化的方法，它允许开发各种类型的系统，包括离散控制系统。然而，它缺乏一个系统的方法来开发这种类型的系统，它阻碍了事件B的适用性。我们的贡献是这样一种方法，它是在本文中。我们提出的方法集中在一组应该被正式模型捕获的元素上，一个他们应该被介绍的顺序。我们的方法的关键方面是首先对环境的所需行为进行建模，然后引入控制器以适当地控制环境。 它的优点是这种发展的每一步都是由现有的信息决定的目前为止，包括要求。我们认为，有一个明确的发展战略，在设计过程的早期将有助于开发人员在生产高质量的模型，未来的软件系统。关键词：事件B，形式化建模，细化，开发策略，系统开发。1引言Event-B [2]是一种用于离散过渡系统的建模方法，该系统通过构造而它的应用范围从顺序程序、并发程序到分布式系统。特别是，事件-B是为数不多的建模方法，其范围内的控制系统之一。更重要的是，事件B中的此类系统的开发包括环境的模型，这对于保证未来系统的正确性是必要的因此，在Event-B中开发系统是一项复杂的任务，涉及系统的多个方面的管理，包括环境。Event-B的一个核心方面是使用逐步细化来降低系统建模的复杂性。”[2]在《易经》中，作者认为：“先有先有，后有后有。1电子邮件地址：shudon@student.ethz.ch2电子邮件地址：htson@inf.ethz.ch[3]本文作者由DEPLOY项目（http://www.deploy-project.eu）赞助。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.01858S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）57^在实际建模任务中，开发人员应该设计一个细化策略，指定每个细化步骤的细节将被引入模型。然而，提出一个好的和有用的改进策略，这有助于系统的开发，是一项具有挑战性的任务。需要有指导方针来设计这种改进战略。为了开发控制系统，Butler在所谓的食谱[3]中提出了建模指南。在[7]中报告了用于开发巡航控制系统的食谱的应用我们的方法和食谱的更多的比较见第5节。在本文中，我们提出了我们的发展战略，在一些关键方面与食谱不同（见第5节）。 在第2节中，我们首先概述了事件B符号;在第3节中，我们解释了我们的策略，并将其应用于第4节中的控制问题四、最后，我们讨论我们的结果在节。五、第二章事件B建模方法事件B由抽象机器的专用符号支持，抽象机器是开发方法的中心对象。它支持正式规范的制定及其细化。我们在本节中简要概述事件B的一些基本方面。关于事件B的完整细节，我们请读者参考[2]。质量标准在Event-B符号中，机器的特征在于由一些变量v建模的状态空间和由一些事件建模的转换状态变量v受某个不变量I（v）的约束事件evt具有以下形式：evt =任何p，其中G（p，v）然后S（p，v，vJ）结束，其中p是参数列表，G（p，v）指定使能条件，S（p，v，vJ）是动作。专用没有参数和保护的事件被用作初始化。动作S（p，v，vJ）包含几个应该同时发生的赋值。 每个赋值可以采用以下三种形式之一：v：= E（p，v），v：∈E（p，v），或v：|P（p，v，vJ）.第一种形式确定性地将表达式E（p，v）的值赋给v，而第二种形式非确定性地将E（p，v）中的某个值赋给v。 最后一种赋值形式是最通用的。 它分配到v的某个值满足前-后谓词P（p，v，vJ）。一台机器是相容的，如果它的不变量在任何给定的时间保持不变。在实践中，这是通过证明不变量是由初始化建立并由其所有事件维护来保证的。细化精化是一种众所周知的技术，用于降低开发正式模型的复杂性一开始是一个抽象的机器捕捉系统的一些核心方面，随后通过添加更多具体的细节来完善机器S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）5759to the model模型.当优化一台机器时，可以引入新的变量和新的事件。必须证明具体机器和抽象机器之间的一致性。在实践中，这是在每个事件的基础上进行的。具体机器的事件是抽象事件的细化，如果加强了警戒，具体事件的动作可以由抽象事件的动作来模拟工具支持在Event-B中进行开发得到了罗丹平台的支持[1]。这是一个内置工具集，包括支持构建Event-B模型，证明其一致性，并为它们制作动画。3发展战略尽管Event-B是一种强大的建模方法，但它缺乏开发不同类型系统的系统方法。我们在这里提出了一些指导方针，我们称之为发展战略，控制系统的开发与他们的环境模型。环境和控制器以双向方式通信：控制器经由各种传感器从环境接收输入;此外，控制器经由各种致动器产生输出以改变环境。这种相互作用如图1所示。传感器执行器Fig. 1.环境与控制器我们的发展战略包括四个不同的阶段。请注意，每个阶段都可以通过几个改进来开发。第一阶段：按照环境应该表现的方式对环境进行建模。第二阶段：对执行器进行建模，以控制环境的变化。阶段3：将传感器与控制器一起建模。阶段4为控制器建模一些合适的调度器。第一阶段的目标是根据需求文档描述具有所需属性的环境。在这个阶段，我们完全省略了控制器，专注于全局安全属性以及物理组件如何协同工作以实现这些属性。在阶段2中，引入致动器作为控制器将检测环境的手段，使得物理组件彼此正确地交互。这反过来又对如何设置致动器施加了一些约束直到第二阶段，通过执行器对环境的所有控制都是在整个系统的完美信息下完成的由于这是不现实的，第三阶段的目标是控制器S环境60S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）57在被观察部件和控制器之间插入传感器这强制执行控制器的适当规范。在阶段4，我们可以向控制器引入调度策略目的是优化其效率。方法的好处在第1阶段的开发中，对系统的理想安全特性进行了建模我们可依赖翻新工程于发展期间保存该等物业在阶段1中捕获的安全属性用作根据需要引入致动器（阶段2）以及继而引入传感器和控制器（阶段3）的指南。这样，控制器及其接口被引入作为维持系统中的安全性的问题的解决方案。因此，致动器的作用是迫使环境按照我们模拟的方式运行。不久之后，传感器的引入将回答这个问题：在执行器之前引入传感器在我们安排收集上述信息之前，找出它需要什么信息通过决定在开发结束时引入调度，我们方便了控制器的设计：模型不受调度细节的影响。 我们可以有单独的模型对应不同的调度算法。4信号控制系统在本节中，我们首先介绍信号控制系统的需求文档，然后描述我们的正式开发，应用我们提出的开发策略4。4.1需求文档我们的目标是在一个特定的火车站开发一个信号控制系统。该系统的概览可以在图2中看到。在下面，我们给出一组对火车站管理的合理要求。它们被定制来让我们解决一些有趣的问题。为了简单起见，有些现实主义被抛弃了我们在本文中只试图解决几个问题。我们的第一组要求涉及列车和网络拓扑。ENV0车站在入口和出口之间有多个站台。ENV1一列火车占用不超过一个街区。4该模型是利用罗丹平台开发的，可在http：//deploy-eprints上查阅。 ecs.soton.ac.uk/308/。S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）5761=入口阻断传出阻滞入口信号输入开关输出开关平台块图二. 信号控制系统ENV2轨道是单向的，即列车通过入口区进入车站，通过出口区离开车站下一个要求涉及位于车站两端的道岔。有两个开关连接入口和出口块到一些平台，相应地称为入口开关和出口开关。ENV4如果进站道岔设置在某个站台区段，则在入口区段的列车只能进入该站台区段。同样，对于输出开关。我们假设开关瞬间改变位置。该系统最重要的特性是安全性：该系统必须保证列车不会相撞。这是通过排除两列列车同时出现在同一区段来确保的。SAF5两列火车不能在同一区段。在这个简单的例子中，我们对证明火车不会脱轨不感兴趣。这样做会使开发复杂化，并转移对我们方法说明的注意力。在车站的两端安装两个（灯）信号机，分别称为进站信号机和出站信号机ENV6有两种信号，要么是红色，要么是绿色。假设ENV7列车在红色信号时停车。控制器接收来自各种传感器的输入，并通过致动器输出其命令。ENV8有传感器检测一个区块是否被占用。ENV9有传感器检测信号的状态。ENV 10传感器反映相应部件5的当前状态.我们设计了一个控制器，用于改变连接到某个平台的开关位置，并将信号从红色变为绿色。当火车经过时，信号灯会自动由绿变红[5]这一假设并不代表我们的方法的适用性。62S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）57到达当ENT∈/OCC然后OCC：=OCC{ENT}端搬进来任意p，其中p∈/OCCENT∈OCC然后OCC：=（OCC{p}）\{ENT}端ENV11对于每个信号，控制器都有一个执行器来命令信号从红色变为绿色。当火车经过时，信号灯由绿色变为红色。ENV13对于每个交换机，控制器都有一个致动器，用于命令交换机切换到特定平台。4.2第一阶段该环境的模型在第一阶段，我们建立一个环境模型。我们将按照以下顺序逐步介绍系统的细节：块、开关、信号和列车。我们为Event-B模型采用以下约定，以明确区分不同的建模元素。• 环境变量和事件用大写字母表示。• 控制器变量和事件的小写前缀是ctr。• 传感器变量以小写形式由snsr前缀。• 执行器变量在小写形式中由act前缀。街区。我们指定了包含入口（ENT）、出口（EXT）和平台块（PLFS）的块集（BLOCK）这符合我们的要求ENV0。 在初始模型中，变量OCC用于记录集合被占领的街区。最初，OCC被分配为空集合。有四个不同的事件，即ARRIVE、MOVE IN、MOVE OUT和LEAVE，用于对如何更改块状态的不同情况进行建模。到达：ENT被占用（因为到达的火车）。移入：ENT变为无人，站台变为有人（由于列车驶入车站）。移出：EXT被占用，站台被占用（由于列车移出车站）。离开：EXT变成无人（因为离开的火车）。由于这些事件之间的对称性，我们只呈现MOVE IN事件然后，他们的到来，以及随后的改进。开关。在此细化步骤中，我们引入变量IN SW和OUT SW来对位于车站两端的两个道岔进行建模。每个交换机的状态表示它们连接到哪个平台块。这符合我们的ENV3要求。最初，开关被任意设置到任何平台。S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）5763搬进来当IN SW∈PLFS\OCCENT∈OCC然后OCC：=（OCC接口{INSW}）\{ENT}不变量：在v20中：ENTSGN=GRN输入SW∈/OCC我们只需要调整事件MOVE IN。它的参数p是用输入交换机连接到的平台实例化的。这符合ENV4要求。该步骤通过提供改变开关的手段来完成。 事件介绍了TURN IN SW和TURNOUT SW，我们让选择任意。我们专注于Turn In SW及其改进。转入SW开始IN SW：∈PLFS端信号。在这一改进步骤中，我们引入了位于车站两端的信号ENT SGN和EXTSGN。信号是红色（表示禁止通行）或GRN（表示允许通行）。这符合ENV6要求。最初，两个信号都是红色的。我们相应地细化了MOVE IN事件，通过使用ENT SGN而不是直接引用ENT块的状态来细化其守卫。这也反映了列车遵守信号的要求（ENV7）。然而，这个保护替换只有在它构成一个加强时才有效，我们通过引入以下不变量来确保这一点。为了保持inv 2 0，我们确保一旦由in-switch指定的平台被占用（ENV 12），信号就变成红色。 同样为了保护inv2 0，我们相应地加强了TURN IN SW的保护搬进来当ENT SGN=GRNENT∈OCC然后OCC：=（OCC接口{IN SW}）\{ENT}ENT SGN：=红色端转入SW当ENT SGN=红色然后IN SW：∈PLFS端有两个新事件可以更改信号的状态，即允许进入和允许退出。我们在这里只显示ALLOW ENTRY，考虑inv2 0。64S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）57›→∈不变量：在v31中：<$t1，t2·t1∈dom（POS）<$t2∈dom（POS）<$t1/=t2<$POS（t1）/=POS（t2）inv3 2：ran（POS）=OCC在v30中：POS∈TRAIN→›BLOCK允许输入当INSW∈/OCC然后ENT SGN：=GRN端火车。在环境模型的最后一个改进中，我们将列车引入系统。关于列车的安全属性都与它们的位置有关，因此这是一个很好的新变量候选者。 因此，引入POS以将每个列车映射到其所在的唯一块（如inv3 0所述），与ENV 1一致。为了排除碰撞的可能性，也就是说，为了执行SAF 5，我们现在可以引入inv3 1，它声明每个列车在其块6上是单独的。最后，为了与变量OCC保持一致，我们引入了inv3 2，以便只有列车可以占用块7。在该模型中，诸如“转向西南”和“允许进入”等事件保持不变，因为它不直接与列车位置交互。 我们相应地细化了MOVE IN和ARRIVE事件，以包括如何更新列车位置搬进来任何twhereENT SGN=GRNt∈dom（POS）POS（t）=ENT然后OCC：=（OCC接口{IN SW}）\{ENT}ENT SGN：=红色位置（t）：=IN SW到达任何twhereENT∈/OCCt∈/dom（POS）然后OCC：=OCC{ENT}POS（t）：=ENT端最后，inv3 2使我们能够重写MOVE IN的保护，如图8所示。4.3第二阶段致动器在第一阶段结束时，我们有一个理想化的环境模型，指定物理组件应该如何协同工作我们引入了一些执行器，即，未来控制器的输出，以命令环境组件的状态的适配，使得环境的正常行为被强制为建模的行为。开关致动器用于向开关发送命令以改变为6结合inv3 0和inv3 1，POS是一个单射函数，即POS∈TRAIN>BLOCK。7原则上，我们可以从模型中排除OCC。然 而 ，我们避免这 样 做，因为OCC捕获了一个有用的抽象，我们仍然可以在整个开发过程中使用它8注意，MOVE IN的最后两个保护可以重写为tENTPOS. 然而，我们更愿意使用两个单独的子句，指定（1）t是系统中受监控的列车，（2）t位于耳鼻喉科。S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）5765（abs）TURN IN SW当ENT SGN=红色然后IN SW：∈PLFS端（cnr）TURN IN SW当在sw中操作= TRUE然后IN SW：=act in sw plfact in sw：=端开关中的时钟触发器任何p其中在sw= swENT SGN=红色act ent sgn= 0p∈PLFS然后在sw中操作：= TRUE在sw plf中操作：=p端ctr chg ent sgn当act ent sgn= 0INSW∈/OCC在sw= sw然后act ent sgn：= TRUE端一个特定的平台（ENV13）。重点研究了开关的执行机构。两个新的变量actin sw和act in sw plf用于对执行器进行建模：前者是一个布尔值，用于指示设备是否有挂起的命令，后者指定开关应该切换到哪个类似地，信号执行器用于发送命令以将信号设置为GRN（ENV11）。信号致动器被建模为一个布尔值，分别用于进入信号的act ent sgn和用于退出信号的act ext sgn事件TURN IN SW使用来自执行器的命令进行相应的细化。混凝土防护装置规定，控制器有一个命令来改变输入开关。因此，输入开关按命令设置到特定平台。开关改变后，执行器复位。事件ALLOW ENTRY的定义类似。我们现在引入不变量来确保守卫的替换确实是一种加强。不变量：inv4 0：在sw= TRUE时动作SGN =RED在V41中：actentsgn=TRUE_INSW∈/OCC最后，我们创建了新的控制器事件，负责通过执行器向输入开关（sw中的触发器）和输入信号（ctr chg ent sgn）发送命令。sw中的事件触发器规定，当进入信号为红色且两个执行器均在sw中动作且actent sgn未设置时，可以设置执行器在sw中动作以指示开关切换到任何平台p事件ctr chg ent sgn模拟了执行器act ent sgn可以设置为命令进入信号改变的事实到GRN，当在开关点到未占用的平台并且两个致动器在sw中动作和在sgn中动作都未被设置时。注意，这些事件的守卫保证新引入的不变量得到维护。66S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）574.4第三阶段传感器和控制器我们现在准备介绍传感器，并假设它们反映实际物理组件的状态。 这很简单，我们 为传 感器 添加 变量 ： 分别 对应 于块 的传 感器 、进 入信 号和 退出 信号（ENV8、ENV9）的snsr occ、snsr ent sgn和snsr ext sgn。这些新变量与使用不变量的旧变量粘合在一起，例如snsr occ=OCC，对应于要求ENV10。在控制器事件（例如，canceltrigger out sw）中，对物理组件（例如，OCC）状态的引用被相应的传感器（在本例中为snsr occ）取代。最后，由于IN SW用于ctr chg ent sgn的保护中，所以当发送用于改变进入信号的命令时，控制器需要知道输入开关的状态。控制器保持输入开关的状态的副本，其变量为csw。请注意，变量ccinSW不一定反映IN SW的当前值。实际上，我们只需要它们在没有用于输入开关的致动器命令时是相同的。当控制器命令相应的开关随着SW中的事件触发器改变时，SW中的事件触发器被更新。4.5第四阶段调度在第三阶段结束时，我们有一个信号控制系统的模型，包括它的工作环境，保证满足我们的安全要求。然后，我们可以为我们的控制器施加额外的调度算法，以优化其执行。在我们的Event-B模型中，它仅仅是通过加强控制器事件的保护来完成的。 作为一个例子，我们在这里展示了sw中事件触发器的优化，• changesopronounce到一个新的免费平台，即p∈/snsroccp=/• 仅当入口块被占用时，即ENT∈snsr occ。在西南部，以及对于更复杂的调度算法，可以通过迭代来采用策略：环境(i) 从环境的角度描述调度算法。(ii) 指定如何在执行器方面实现这种算法。(iii) 设计传感器和控制器实现算法。5结论我们已经提出了我们的发展战略，开发控制系统连同他们的环境模型。我们的策略从环境建模开始，然后引入执行器，然后对控制器和传感器进行建模。最后，进一步的调度细节施加在控制器上作为系统的优化步骤。应用我们的发展战略，减少了建模这种类型的系统的困难，导致模型，S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）5767易于理解和验证。我们通过开发一个简单的信号控制系统来说明我们的方法。尽管目前还没有Event-B的代码生成器，但我们最终模型中的控制器变量和事件足够具体和清晰，可以用作软件底层设计。我们的发展战略最初受到Laurent Voisin开发电梯系统的启发，该系统已被用作苏黎世联邦理工学院我们已经将该方法应用于几个这类系统，包括Abrial [ 2，第2章]中“桥上的汽车”示例的重新开发我们的方法从根本上不同于Abrial所采取的由内而外的与我们的方法相反，Abrial首先对控制器进行建模，然后引入环境。尽管这两种方法都可以用于开发这种类型的系统，但我们的由外而内方法更具建设性：我们不是先定义一个控制器，然后证明它适合环境，而是使用需求来推导控制器必须满足的约束，然后我们继续相应地构建它。我们的发展战略与Butler的[ 3 ]相似环境的模型。这两种方法的区别主要在于执行器和传感器的引入顺序不同，在我们的方法中，执行器在传感器之前。我们认为，这更清楚地表明了一种正确的设计。这是由我们的反向推理所引起的：我们想从对控制器输出的约束中推导出控制器及其输入的设计。 我们认为这种方法更简单，并为设计提供更强的指导，类似于使用最弱前提的推理[4]。控制系统的验证已经使用其他形式化的方法进行了研究。Hansen使用VDM验证了铁路联锁模型[5]。然而，本文只建立了一个模型的环境，没有控制器。Haxthausen和Peleska提出了一种使用RAISE开发分布式铁路控制系统的方法[6]。他们的方法包括两个阶段。在第一阶段，环境和控制器的模型在全球范围内共同开发。他们的第二阶段集中在设计一个分布式控制器对应的模型在第一阶段。我们的发展策略可被视为在其第一阶段发展该模式在我们的示例中没有捕获的一个方面是假设。典型地，它们涉及通信速度和控制器的响应。可以证明，使用我们的发展战略，这些假设在正式发展过程中自然产生，否则很难找到先验。此外，我们还专注于开发具有某些关键安全特性的系统。开发满足活性属性的系统，例如所有列车最终必须离开车站，将需要额外的建模准则。引用[1] J-R Abrial，M. J. Butler，S. Hallerstede，T. S. Hoang，F. Mehta和L.瓦辛 Rodin：Event-B中建模和推理STTT，12（6）：44768S. Hudon，T.S.Hoang/Electronic Notes in Theoretical Computer Science 280（2011）57[2] 让·雷蒙德·阿布里尔事件B建模：系统与软件工程。剑桥大学出版社，2010年5月。[3] 迈克尔·巴特勒走向控制问题的建模和细化的食谱。工作文件，http://deploy-eprints.ecs.soton.ac.uk/108/，2009年5月[4] Edsger Dijkstra 程序设计的一门学科。Prentice Hall International，Englewood Cli Jersey，新泽西州，1976.[5] 克尔斯滕·马克·汉森。 铁路联锁模型的验证。 在Maurice Naftalin，B. Tim Denvir和Miquel Bertran，编辑，FME，LNCS第873卷，第582Springer，1994年。[6] 安妮·伊丽莎白·哈克斯特豪森和扬·佩莱斯卡。分布式铁路控制系统的形式化开发和验证。 IEEE Trans. 软件工程师，26（8）：687[7] S. Yeganefard，M. Butler和A.雷扎扎德通过事件B中巡航控制系统在NFM 2010会议记录中，第182