大型系统设计的方法学过程：两个工业案例研究

84理论计算机科学电子笔记66第二次（2002年）网址：http://www.elsevier.nl/locate/entcs/volume66.html20页大型系统设计的方法学过程：两个工业案例研究。Nérique Lopez，MarianneSimonot，V'eroniqueVigui'eDonzeau-GougeCedricResearchLaboratory，ConservatoireNationaldesArtsetM'etiers，292 Rue Saint-Martin，75141 Paris Cedex，France.电子邮件：（donzeau，lopezne，simonot）@cnam.fr摘要本文介绍了两个例子，从工业案例研究，已指定使用事件系统的方法。 元件规格，采取前-后公式的形式，已被导出。给出了保证整个过程正确性的 约 束 条 件 。1介绍我们的目的是提出一个方法的过程，可用于整个系统的开发。我们根据系统必须满足的性质来定义系统这个过程导致我们建立两种数学模型：事件模型和操作模型。它们定义了整个系统的形式规范。这些模型被证明是一致的，并确保了整个过程的正确性，即每个组件实现的正确性和整个系统实现的正确性。我们所考虑的应用程序与其环境有很大的交互。它们可以使用现有的硬件和软件组件。解决的问题：第一个问题是这种具体化需要大量的信息，这使得有必要在表达的想法中引入一定的层次结构。这可以通过两种方式实现：通过定义更抽象的方面并逐渐关注细节;通过将属性分组到特定类别（描述组件之间以及与环境之间的交互的属性，以及对一个组件本地的属性，如功能属性）。我们使用精化技术[Back 88]，[Morg 90]，[Abr 96-1]，[But 96]来支持抽象，即。来介绍细节和表达一些设计决策。第二个问题是如何指定系统与其环境的相互作用2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。LOPEZ，SIMONOT，VIGUIE85我是说。趋势是建立一个封闭的模型[Abr 96-2]，其中包括整个环境。然而，这个模型可能非常复杂。在我们的方法中，我们开发了一个封闭的模型，它只指定系统与环境的相互作用。此外，细化一个封闭系统可能会导致程序无法实现我们心中的规范[Lop，Sim，Don 00]。选择：形式规范语言必须允许非确定性规范的表达，并且必须得到有效证明的支持，因此我们既不合并不同的逻辑，也不引入新的逻辑。我们在很大程度上依赖于现有的由工具支持的经过验证的方法。我们采用集合论以及精化技术，因为它们被封装在实际的工具[Atelier B]，[B Toolkit]中。过程：我们从一个用自然语言编写的非正式规范开始，它描述了系统必须满足的所有属性。领域专家参与本文档的详细说明和验证在介绍系统细节时，可以做出一些实现选择：例如，重用具有良好定义接口的现有设备。然后，我们逐步建立了一个事件模型，它只描述了系统与其环境之间以及不同组件之间的相互作用。它表达了我们对环境的假设。我们只保留那些表示相互作用的初始性质这一过程由事件细化技术控制，如[Lam，Sha90]，[But 96]，[Abr 96-2]，[Back，Kur 88]中所在此之后，事件模型被转换为用于指定组件的共享模块。该模块提供系统的外部和内部通信机制。它被称为接口模块。 粗略地说，模块是指一组程序规范，可以细化为顺序的程序实现。最后，每个组件的规格分别编写。它包含了仅与此组件相关的非正式规范的属性，因此尚未考虑。组件规范被用作顺序程序的通常精化过程的起点[Back 88]，[Abr96-1]。整个过程的正确性见[Lop 02]。在这篇文章中，确保这种正确性的条件将只是轻轻触及。在本文的其余部分，我们将处理从工业案例研究中提取的两个例子，这些案例是使用[Atelier B]指定和部分证明的它们在此工具的语法中呈现，并添加了一些注释以帮助读者。然而，B方法不包括我们用途：共享模块和辅助变量这两个重要的这些概念在[Lop 02]中被他们倾向于将B方法的使用扩展到并发系统和分布式系统。第一个例子说明了我们用来指定一个大型系统的方法第二示例LOPEZ，SIMONOT，VIGUIE86∃∧∃∧∪∃∧∪∀ ∃ ∧ ∧⇒ ∃ ∧∧±说明了我们用来导出组件规格的方法此示例的事件2基于事件的规范：M'et'eor地铁线的乘客换乘功能Meteor是巴黎新建的一条全自动化地铁线路。 该线路由列车和到达/离开站台组成。火车和站台都有门。乘客换乘功能1必须确保乘客的安全，这是建立在四个独立的原则上的P0交易所不能产生不安全的情况。P1为保证旅客P2如果火车和站台是封闭的宇宙，乘客是安全的。P3如果发生危险情况，乘客应随时有可能离开列车，以获得安全的环境。可以识别几种乘客交换：通常的乘客交换，以及在检测到危险情况时发生的紧急疏散。一旦发生危险，必须立即进行疏散。2.1回顾事件事件规范采用a的形式。G（x，a）A（x，a，xJ）.警戒限制事件的发生，而行动则规定其效果。变量a允许表达外部非确定性，即，环境提供的外部价值保护G（x，a）定义了事件可以被观察到的状态，动作A（x，a，xJ）与观察之前和之后的系统状态一个事件的具体语法（在[Abr 96-2]中）是任何a，其中G（x，a）则Sx，a，其中Sx，a是A（x，a，xJ）的平移的例如，xJ=x a可以转化为x：=x a。事件细化。设E1（x， XJ）具有a的形式. G1（x，a）A1（x，a， XJ）和E2（w，WJ）的形式为a. G2（w，a）A2（w，a，wJ），两个事件的具体化。它们被定义在两个不同的状态空间上。设J（x，w）为a在这两个空间之间定义的总关系，公式E1JE2= defx，w，wJ。a. （J（x，w）G2（w，a）A2（w，a，WJ））a，XJ. G1（x，a）A1（x，a，xJ）J（xJ，wJ）表示用E 2观察到的所有状态变化也用E1观察到的事实。1本案例研究由RATP和Matra Transport International提出在CNAM计算机研究中心（实验室）CEDRIC）、RATP、MTI（SIEMENS）和STERIA根据DJ.0246/98合同提供的服务。[2]这个演示是这个问题的简化版本-更详细的描述在[Lop 02]，[Lop 99]中提供。LOPEZ，SIMONOT，VIGUIE87∈∧--事件系统。一个事件系统Ss =（x，IS，C，E i）由一个表示系统状态的共享变量x、一个表示系统静态属性的不变量IS、表示系统的规范C和事件集Ei（i 1.组成。这就定义了动力学。这样的系统是变迁系统，其初始状态由初始化定义，其变迁由事件定义系统一致性。一个事件系统被称为是一致的，如果不变量是由初始化建立的，并由每个事件保存。系统完善。 设S1和S2是两个事件系统，J（x，w）是它们变量之间的全关系，S1被S2（S1±JS2）精化，如果S2的每个事件是S1的相应事件的精化，并且如果初始值为S2的初始化是对S1的初始化的细化。相应的证明义务由实际工具产生。添加新事件。 根据[Abr 96-2]，[Lop 02]，在精炼期间可能：• 添加新事件。为此，我们只需假设新事件存在于抽象系统中，并以真跳跃作为其具体化。跳过意味着新事件不修改抽象系统的任何变量。这意味着当引入一个新变量时，细化必须包含修改该变量的所有事件这限制了引入事件的方式• 拆分事件。这种分解使我们能够更精确地观察事件。为了做到这一点，我们可以假设在抽象系统中，抽象事件E可以根据需要被重复多次，并且分解中的每个事件都必须是E的一个精化。2.2第一模型这个模型引入了系统的主要概念：列车tt，站台qq，以及它们可能的状态（变量）：不安全（td，qd）或安全（tt td，qq qd）。在这个层次上，只能表达属性P0。我们可以观察到五个事件：- 修改变量td的UnsafeTrain、SafeTrain。- 修改变量qd的UnsafePlatf、SafePlatf。- 对环境无影响，可随时启动的转移请注意，转移可以在任何时候发生，而不仅仅是在安全的情况下还请注意，属性P0是通过Transfer动作不修改系统状态这一事实来表示的。LOPEZ，SIMONOT，VIGUIE88流星系统1. 1设置tt;qq/* 列车、线路站台 */变量td，qd/*不安全列车和站台 */不变tdttqdqqINITIALISATIONtd，qd：=，/* 线路安全 */事件Ttransfer=0SELECTT RUE/* 交换总是可观察的。*/然后跳过/* 安全性未修改（P0）。*/ End;UnsafeTrain=/*Asafetrainbecomesunsafe*/UnsafePlatf=/*q1becomesunsafe*/ANYt1WHEREt1∈ttt1∈/tdANYq1WHEREq1∈qq<$q1∈/qd则td：=td{t 1}则qd：=qd{q 1}END; END;安全Train=/*Anunsafetrainbecomessafe*/SafePlatf=/*q1becomessafe*/ANYt1 WHEREt 1∈tdANYq 1 WHEREq1 ∈qd则td：=td− {t 1}则qd：=qd− {q 1}结束;结束该模型的一致性证明由Atelier B生成和发布我们可以使用这个模型证明其他属性。例如，无死锁是由以下事实暗示的：在不变量下，守卫的析取总是为真。我们还可以证明系统应该允许的事件跟踪的属性：例如，可以在任何时候观察到传输2.3二模型该模型引入了表示属性P1所需的锁定序列的概念锁定的列车完全停止，并开始移动，一些行动需要执行之前。变量ti对锁定列车的集合进行建模。 因此，两个新事件介绍了LockedTrain和UnlockedTrain在这个层面上，我们要分别观察两种交换：正常交换和其他情况。为了区分这两种情况，我们区分了在正常条件下进行乘客交换的列车：变量ttv。此划分是通过分解事件Transfer完成转换为两个事件EndPassExch（正常交换）和转账1（其他交易所）。必须添加事件StartPassExch才能修改ttv。它允许观察正常乘客交换的开始当列车在ttr时，进行正常的交换。因此，ttv仅包括满足该性质的列车。为了表达这一点，我们引入了一个从列车到站台的偏函数t q，变量qtv表示在正常情况下进行乘客交换的列车LOPEZ，SIMONOT，VIGUIE89如果列车停在站台前，StartPassExch被激活，因此，t q出现在其防护中。引入了其他修改此变量的事件：从平台上返回和到达平台上。性质P1是系统的不变量。Meteor 1系统的前四个事件。除了我们刚刚介绍的事件之外，这里还包括1个事件。前四个事件仍然不同步。新事件同步如下：LockedTrain→Transfer1 → UnlockedTrain到达平台→锁定列车→开始PassExch→结束PassExch→解锁列车→从平台解锁LockedTrain →UnlockedTrain这种同步性的保证是通过以下方面的证明义务获得的-只有守卫。流星系统1. 2个变量td，qd，/* 不安全的列车和站台 */t q，/*列车在站台前 */ttr，/* 列车在换车 */ttv， qtv，/* 列车和站台进行乘客交换 */ti/* 锁定列车 */INVARIANTtdttqdqqt q∈tt>qq<$ttv<$ttr<$ti<$tt<$/* 包括（P1）*/ttv∈dom（t q）<$qtv=t q[ttv]初始化t q，ttr，ttv，td，ti，qtv，qd：=，事件不安全的T雨=雨. . .UnsafePlatf=不安 全 .安全T雨=雨. . .SafePlatf=安 全 .StartPassExch=0/*t1startsaTtransfer*/EndPassExch=0/*t1finnishesaTransfer*/ANYt 1 WHERE ANYt 1 WHEREt1∈ti<$t1∈/ttr<$t1∈ttvt1∈dom（tq）<$tq（t1）∈/qtv/*t1isinTransfer*/则ttv，qtv，ttr：=ttv{t1}，则ttv，qtv，ttr：=ttv−{t1}，qtvtq[t1]，ttr{t1}qtv−t q[t1]，ttr−{t1}END; END;Ttransfer 1=1ANYt1WHEREt1∈tit1∈/ttv/*t1不在传输中*/THENSKIP/* 传输结束 */结束语：LOPEZ，SIMONOT，VIGUIE90→LockedTrain=/* 未锁定的列车变为锁定 */ANYt1其中t1∈tt<$t1∈/ti则ti：=ti<${t1}结束语：ArrivalToPlatf=/* 火车到达（空闲）站台 */ ANYt 1，q 1WHEREt1 ∈ttq1∈qq<$t1∈/dom（tq）<$q1∈/ran（tq）<$t1∈/ti则tq：=t q<${t1<$→q1}END;UnlockedTrain=/* 锁定的列车变为解锁 */ANYt1其中t1∈ti<$t1∈/ttr则ti：=ti−{t1}结束语：出发FromPlatf=100/* 一列火车离开站台 */任何地方t1∈dom（t q）<$t1∈/ti则t q：={t1}<$t q结束语：2.4三模型在这个模型中，我们观察门的正常打开 它引入了安全属性P2，其可以重写如下：（P2.1）未关闭的列车处于乘客换乘状态，（P2.2）未关闭的站台是当前正在进行乘客换乘或处于安全状态的站台。 我们引入开放列车和开放平台qo以及四个事件OpenedTrain，ClosedTrain，OpenedPlatf，ClosedPlatf，修改这些变量。这些事件详细介绍了trans-位置开始PassExch结束PassExch。他们的守卫定义了以下同步：StartPassExch→OpenedTrain→OpenedPlatfClosedTrain封闭平台f→EndPassExch只有在站台安全的情况下，站台门才会打开在这里，我们引入变量qs，因此，两个事件SafeZone和UnsafeZone允许修改此变量。这些事件详细描述了一个平台的开放SafeZone必须出现在OpenPlatf之前，UnsafeZone必须出现在ClosedPlatf之前。流星系统1. 3个变量td，qd，t q，ttr，ttv，qtv，ti，to， qo，/* 开放的列车和站台 */qs，/* 安全平台区域 */LOPEZ，SIMONOT，VIGUIE91不变td<$tt<$qd<$qq<$t q∈tt>qq<$ttvttrtitt/* 包括（P1）*/ttv∈dom（t q）<$qtv=t q[ttv]<$至/* 包括（P2.1）*/qoqqqs<$qq<$qo<$qtv<$qs/*（P 2.2）*/初始化t q，to，ttr，ttv，td，ti，qo，qtv，qd，qs：=，事件不安全的T雨=雨. . .UnsafePlatf=不安 全 .安全T雨=雨. . .SafePlatf=安 全 .启动PassEx ch=0.. .结束PassEx ch=0ANYt 1 WHEREt 1∈ttvt1∈/to<$tq（t1）∈/qoTtransfer 1=0.. .则tt v，qt v，ttr：=ttv−{t1}，qtv−t q[t1]，ttr−{t1}/* 传输结束 */ END;Locked Train=.. .Unl ocked Train=.. .Arri val ToPlatf=.. .Departure FromPlatf=0.. .操作T雨=/*t1becomes操作d*/关闭T雨=/*t1becomes关闭d*/任何t1其中t1∈ttrt1∈/到任何t1其中t1∈到然后到：=到{t 1}然后到：=到− {t 1}END; END;OpenedPlatf=/*q1becomesopened*/ClosedPlatf=/*q1becomesclosed*/ANYq1WHEREq1∈qtvqsq1∈/qoANYq1WHEREq1∈qo则qo：=qo{q 1}则qo：=qo− {q 1}END; END;SafeZone=/*q1zonebecomessafe*/UnsafeZone=/*q1zonebecomesunsafe*/ANYq1WHEREq1q q<$q1∈/qsANYq1WHEREq1∈qs则qs：=qs<${q 1}则qs：=qs− {q 1}END; END;2.5四模型在这个模型中，我们引入属性P3，我们观察到一个紧急疏散。在这种情况下，乘客必须离开列车，因此列车状态必须允许车门打开，并且还必须提供通往安全流通区的通道所有处于紧急疏散状态的列车都由变量teu建模。我们有两个事件可以让我们观察紧急疏散的开始和结束：StartEva和EndEva。新概念：疏散区ze，以及其中的安全区zs。 我们必须能够相对于疏散区定位一列火车;这就是函数t z的作用。修改t z（ArrivingZoneEva和LeavingZoneEva）和zs，（SafeZoneEva）的事件和UnsafeZoneEva）被引入。将平台本地化为疏散区由关系式q z定义。如前所述，事件Transfer1被分解为两个事件：LOPEZ，SIMONOT，VIGUIE92转让2。 EndEva模拟了紧急疏散的结束，StartEva使列车处于疏散状态（teu已修改）。就像以前的系统一样，警卫确保预期的同步。流星系统1. 4SETSze/* 疏散区 */常量q z/* 将平台定位到区域 */ PROPERTIESq z∈qq参与变量td，qd，t q，ttr，ttv，qtv ti，t0，q0，qs，t z/* 列车定位 */teu，zs/* 紧急疏散和疏散区域 */ INVARIANTtdttqdqqtq∈tt>qqttvttrtitt/* 包括（P 1）*/ttv∈dom（t q）<$qtv=t q[ttv]<$to<$ttr<$tt<$/* 包括（P 2.1）*/qoqqqsqqqoqtvqs/*（P2.2）*/t z∈tt参与范围（t z）=ttt q−1;tz qzteuttrttvteu=teutdzszeteutz−1[zs] /*（P 3.1）*/ran（q z）=ze/*（P 3.2）*/初始化t q，t z，to，ttr，ttv，teu，td，ti，qo，qtv，qd，qs，zs：t q=tz∈ttParticipzedom（t z）=ttto=ttr=ttv=teu=td=ti=qo=qtv=qd=qs=zs=事件不安全的T雨=雨. . .UnsafePlatf=不安 全 .安全T雨=雨. . .SafePlatf=安 全 . 启动PassEx ch=0.. .结束PassEx ch=0.. .Locked Train=.. .Unl ocked Train=.. .Arri val ToPlatf=.. .Departure FromPlatf=0.. .O pened Train=.. .关闭T雨=. . .O penedPlatf=0.. .ClosedPlatf=关闭. . .SafeZone=安全区 .UnsafeZone=安全区 .StartEva=/*t1startsanevauation*/ANYt 1WHEREt 1∈tit 1∈tdt1∈/ttr<$tz[t1]<$zs则teu，ttr：=teu{t 1}，ttr{t 1}结束语：EndEva=/*anevacuationisfinished*/ANYt1 WHEREt 1∈teut1∈/tot1∈/td则teu，ttr：=teu− {t 1}，ttr− {t 1}结束语：Ttransfer2=1000ANYt1WHEREt1∈/tttvteut1∈ti/*t1不在传输中*/THENSKIP/* 传输完成 */END;到达区域Eva=/*t1arrivesinazone*/LeavingZoneEva=/*t1leavesz1*/ANYt1，z 1 WHEREt 1∈ttANYt1，z 1 WHEREt 1∈ttt1∈/ti<$z1∈/tz[t1]<$z1∈ze <$z1∈/zst1∈/ti<$z1∈tz[t1]<$z1∈/zs则t z：=t z<${t1<$$> →z1}END;则t z：=t z− {t1<$→z1}END;SafeZoneEva=/*z1becomessafe*/UnsafeZoneEva=/*z1becomesunsafe*/ANYz1WHEREz1∈zez1∈/zsANYz1WHEREz1∈zsz1∈/tz[td]THENzs：=zs{z 1} END; THENzs：=zs− {z 1} END;另一种乘客交换是使用类似的亲，LOPEZ，SIMONOT，VIGUIE93cess.2.6结论在这一点上，我们得到的是系统所需行为的形式化描述它采用事件模型的形式。这个模型描述了一个表示外部行为的自动机。一些安全属性指定系统的静态，另一些则指定动态。这里，P1、P2和P3是静态的，P0是动态的。静态属性嵌入在不变量中。由于事件细化机制，最终规范中有很多事件已逐渐引入这种自上而下的分析使我们引入系统细节，尽管具有类似抽象级别的属性之间的插入顺序或多或少是任意的。例如，可以在正常交换之前或同时此外，精化过程允许我们分裂最终事件系统的一致性证明事件同步通过警卫分发。该应用程序是在AtelierB下开发的。几乎所有产生的证明义务都已自动解除。然而，我们还没有该系统的内部结构每个组件的隔离还没有完成，而且，对于每个组件，我们没有实现。为了说明整个过程，我们将介绍第二个应用程序，该应用程序已被带到实现点3飞行警告系统（FWS）：事件模型3.1介绍这个案例研究-空中客车A340飞机上使用的灯光警告系统（FWS）-是由法国宇航公司提出的。FWS当出现异常情况时，FWS必须决定何时以及如何发出警告信号。本研究的困难之一来自于对最终架构的强制约束：系统必须由两个循环并发过程形成第一个是P1，负责检查所有报警。如果检测到警报过程在预定义的时间段之后确认它如果检测到报警第二个进程P2也必须检查所有警报。它负责发出与第一个过程确认的警报由于两个周期是并行的，因此不可能将应用指定为以下序列：P1; P2。我们必须考虑到P2在P1之前检查报警的事实，因此，在这种情况下，不会发出信号。让我们想象一个警报a在时间t被激活。有六种可能的情况：LOPEZ，SIMONOT，VIGUIE94(i) t... P1 ... P2：报警a在P1和P2检查之前“发生”。报警在其运行周期内由P1处理，由P2处理。发出信号3。(ii) t... P2 ... P1：报警a发生在P1和P2检查之前。报警由P2处理。由于P1尚未检查a，因此在P2的运行周期期间不发射信号。在P2的下一个周期期间将发射a的信号，除非P1在其自己的下一个周期期间在P2之前检查a并检测到a不存在。(iii) P1... P2... 到P2. P1... T：A将在它们的下一个周期中通过两个过程进行治疗。(iv) P1... t... P2：与情况3相同。(v) P2... t... P1：在其运行周期中，P1检查并确认a。P2将在其下一个循环中处理a（除非P1检测到a不存在）。3.2事件模型在这里，我们提出了一个简化版本的案例研究，其中不包括有关的复盖阶段和信号组成的细节。完整的描述在[Lop 96-1]、[Lop 96-2]中给出事件规范的作用是对组件和环境之间的交互进行建模。为此，我们需要警报集合WW和信号集合Ss，以及以下变量：wp：发出的报警集，se：发出的信号集，wc：确认的报警集，We1、Wp1：P1检查并检测到的报警We2、Wc2检查并检测到的报警由P2确认。编号1：计数器。P1的执行周期数。数字2：计数器。P2的执行周期数。在这个模型中，我们观察到以下情况：- 警告情况（与环境的交互）的出现的开始（NewWarning）和出现的结束（EndWarning- 信号的发射（EmittedSignal）的开始和信号的结束（EndSignal）（P2与环境之间的相互作用），报警的确认（ConfirmWarning1）及其结束（AbsentWarning1）（P1和P2之间的交互），P1对报警的检查（检查警告1）（P1和环境），P2对报警的检查（检查警告2P2和环境），3在实际系统中，信号可以被发射，但不能保证这一点，因为一架飞机可能处于许多警报被激活的状态，因此存在竞争[Lop 96-1]。LOPEZ，SIMONOT，VIGUIE95P1 （ BeginCycle1 ） 新 周 期 的 开 始 ， P2（BeginCycle2）新周期的开始此事件模型的构建方法与上一节所述系统FWS 2组Ww，Ss变量wp，se，wc，wp1，Wp 1，We 1，Wc2，we 2，wc 2不变wp，wc，Wp 1，We 1，Wc 2，We 2 Ww电子邮件网络地址1，网络地址2 ∈NAT初始化wp，se，wc，wp1，Wp1，We1Wc 2，We2，wp2：（wp = wp，se = wc，wc = wc，wc = wp，wc，wc，wp 1，we 1 wc 2，we 2，wc 2：（wp= wp，se =wc，wc= wc，wc1 = 0Wp1 =新警告=/*新警报出现*/结束警告=/*警报结束*/ANYwxWHEREwx∈W wwx∈/wpANYwxWHEREwx∈wpTHENwp：=wp{wx} END; THENwp：=wp−{wx} END;EmittedSignal=/*发射新信号*/EndSignal=/*信号的熄灭*/ANYsxWHEREsx∈Sssx∈/seANYsxWHEREsx∈seTHENse：=se{sx}END;THENse：=se−{sx}END;检查警告1=/*P1正在检查警报*/确认警告1=/*P1确认警报*/ANYwxWHEREwx∈W wwx∈/W e1ANYwxWHEREwx∈W wwx∈/wc/*wx 尚未被检查 */THENwc：=wc{wx} END;然后如果wx∈wp则/*警报存在*/不存在Warning 1=0/*P1指示wx不存在*/Wp1，We 1：=Wp 1<${wx}，We 1<${wx}ANYwx WHEREwx∈Ww否则我们1：=我们 1{wx}结束，然后wc：=wc−{wx}结束;结束;BeginCycle 1=N/*P1的新周期*/BeginCycle 2=N/*P2的新周期*/SELECTWe 1 =WwSELECTWe 2 =Ww则W e1， W p1， Num1：=1，1，Num1 + 1则W e2， W c2， Num2：=1，1， Num2 + 1/* 检查所有告警 *//* 检查所有告警 */ END; END;检查警告2=警告/*P2正在检查警报*/一个Ywx其中wx∈W wwx∈/W e2/*wx尚未被检验：wx∈/W e2*/则如果wx∈wcTHENWc 2，We 2：=Wc 2{wx}，Wee 2{wx}/* 警报已确认 */ ELSEWe 2：=We 2{wx} END /* 警报未确认 */结束语：注意，P1和P2之间的相互作用是通过变量wc实现的它由P1修改，由P2访问。还请注意，事件BeginCycle1和BeginCycle2同时删除了分别为we1，wp1和we2，wc2的所有元素：它们模拟了每个周期的开始。如在守卫中所指示的（we1=Ww并且we2=Ww），这些只有当每个过程检查了所有报警时，才能激活事件。4从事件模型到模块：简介事件系统FWS2对系统与环境以及两个进程P1和P2之间的交互进行建模。现在我们将通过这个例子来说明这个过程的结束：从这个事件系统到每个组件的规范，再到接口模块的规范。为了做到这一点，我们必须首先将事件系统转换为模块LOPEZ，SIMONOT，VIGUIE96关于我们关于我们联系我们其将由组件共享它的作用是为每个组件提供与环境交互所需的操作：这就是接口模块。每个组件的规格并非直接来自事件模型。它必须单独制定，并且必须包含组件本身的特性。 这里组件规范可以使用接口模块的一些变量。通过这样做，我们可以将组件的局部属性与整个系统的预期行为这个规范可以在以后进行细化，以实现它。现在我们将逐步说明这部分过程模块和操作。模块规范MS=（x，IM，A，Oi）由表示模块状态的共享变量x、表示模块静态属性的不变量IM、设i ∈ 1，则模和运算集O i是一个集合。n定义动力每个操作Oi都采用一个pre-post specification的形式（Pi（x），Qi（x，xJ））.在该工具的语法中，它采用PreP（x）THEN S的形式，其中S是广义替换。因为有一个翻译的gener-将替换分解为前后谓词[Abr 96-1]，它对应于程序指定的通常前后公式这样的模块是转换系统，其初始状态由初始化定义，其转换由操作定义从语义的角度来看，模块和事件系统是等价的。模块的一致性一个模块被称为是一致的，如果不变量是由初始化建立的，并由每个操作保存。重新定义。一个模块M被M1精化，如果M的每个操作都被M1的相应操作精化，并且如果M的初始化被M1的初始化精化。一个运算，即一个程序规范（P，Q），被另一个规范（R，S）所定义，如果对所有程序t，R t S蕴涵P t Q。这些证明义务是由工具产生的。操作和事件之间存在语义上的差异：细化程序规范可以削弱前置条件，而细化事件可以加强保护。模块实现。设M是一个模（x，IM，A，Oi）. M的实现是一组程序t0，t1，.，t n使得：真实t0AIM和 IMPi我不是IMQ i.这些条件加上M的相容性，意味着以下性质：对于所有M，我们有{true}t0;M（t1，...，其中M是if then else、while、sequence（;）和操作O i的组合。换句话说就是不变量被所有模块状态满足模块进口。 我们可以导入一个模块来实现另一个模块[Abr 96-1]。设M是与前面相同的模，M1是（x，IM1，A1，Vi）（其中i∈LOPEZ，SIMONOT，VIGUIE971. k）。每个Vi的形式为（Ri，Si）。为了通过M的输入实现M1，我们有：(i) 为每个Vi提供表达式Mi（O1，.，O n）built with combina- tions ofcalls of O i，(ii) 为了证明Vi±Mi（O1，.，O n）。如 果 导 入 的 模 块 M 具 有 实 现 ， 即 一 组 程 序 t0 ， t1 ， . ， tn 使 得 ：{true}t0{AIM}，和{IMP i}t i{IMQ i}，上述条件确保，对于所有M：{true}t0; M（M1（t1，...， t n），.， Mk（t1，…，t n））{IM1}。5迈向接口模块：第一步5.1将事件转换为操作事件系统规范允许我们观察一个完整的系统--一个不与观察者交互的因此，系统规范模拟了一个封闭的宇宙。一个接受输入并产生输出的程序并不是一个封闭的宇宙。连接这两种方法的方法是将事件系统视为观察程序行为的工具如果操作允许的每个转换也是对应于该操作[Lop，Sim，Don 00]，[Lop 02]的事件的可能转换，则情况就是这样然后，为了将系统转换为模块，它需要转换每个事件：E= 任 意 a 其 中 G （ x ， a ） thenSx ， a 进 入 运 算[res←−]op（a）=preG（x，a）thenSx，a。我们可以自由添加输出参数。 很明显，在这种情况下，事件系统及其对应的模块定义了同一个变迁系统。可以在事件和操作之间进行更复杂的转换。在这些情况下，必须产生和履行一些举证义务为更多详情，参见[Lop 02]，第5.7章。5.2应用于FWS模块接口是从FWS2获得的，遵循上面定义的转换。机器FWS ENV变量wp，se，wc，wp1，Wp 1，We 1，Wc2，we 2，wc 2不变量wp，wc，Wp1，We 1，Wc 2，We 2<$Wwse<$Ss< $1，< $2∈NAT初始化wp，se，wc，wp1，Wp1，We1Wc 2，We2，wc2：（wp=se=wc=1= 0Wp1 =We1 =Wc2 =WwWe2 =Ww2 = 0）操作新警告（wx）=PREwx∈W w <$wx∈/wpTHENwp：=wp{wx}END;EmittedSignal（sx）=PREsx∈Ss <$sx∈/seTHENse：=se{sx} END;EndWarning（wx）=<$PREwx∈wp则wp：=wp−{wx}END;确认Warning 1（wx）=<$PREwx∈W w <$wx∈/wcTHENwc：=wc<${wx} END;LOPEZ，SIMONOT，VIGUIE98∧∧EndSignal（sx）=PREsx∈SeTHENse：=se−{sx} END;bres←−ExamineWarning2（wx）=<$PREwx∈W w<$wx∈/W e2THEN如果wx∈wc那么Wc2，We 2，bres：=Wc2{wx}，W e2{wx}，T RUE否则我们2，bres：=We2{wx}，F ALSE ENDEND;BeginCycle2=1000PREWe2 =Ww那么我们2，Wc 2，Wc 2：=，AbsentWarning 1（wx）=<$PREwx∈Ww那么wc：=wc−{wx}结束;bres←−ExamineWarning1（wx）=<$PREwx∈W w<$wx∈/W e1THEN如果wx∈wp则Wp1，We 1，bres：=Wp1{wx}，W e1{wx}，T RUE否则我们1，bres：=We1{wx}，F ALSE ENDEND;BeginCycle1=1000PREWe1 =Ww则We1，Wp 1，Wp 1：=N1+ 1END;6朝向接口模块：第二步6.1逻辑和抽象变量所有模块变量都用于表示属性。其中一些模型对象将有效地实现的程序-他们被命名为抽象变量，并有一个操作的内容。其他的只是逻辑上的它们被称为逻辑变量或辅助变量[Aba，Lam 88]。 抽象变量是在模块细化过程中唯一被转换的变量。它们被实施，以及数据细化。逻辑变量不会出现在最终实现中。设M是一个包含抽象变量（a）和逻辑变量（l）的模设M1是当所有出现逻辑变量的表达式都被消去时从M我们想把M1的任何实现作为M的一个实现如果M的每个操作OM具有以下形式，则这是可能的OM=（p（a）pl（a，l），q（a，aJ）ql（a，l，lJ））且满足：阿吉亚湖 （p（a）<$p l（a，l）<$q（a，aJ）→<$lJ. ql（a，l，lJ））。现在考虑M1中的相应运算.它采用以下形式：opM1=（p（a），q（a，AJ））。所以我们有：(i) 一旦OM可以被激活，OM1也可以被激活（先决条件已经被约束）。(ii) 抽象变量a、aJ不依赖于逻辑变量（但l可以依赖于a）。(iii) 在OM的前提下，OM1所能达到的所有状态也都是OM所能达到的。这意味着，在优化过程中，无论做出何种减少影响的实施选择LOPEZ，SIMONOT，VIGUIE99OM1的内部不确定性，它将实现OM的后置条件。这些约束确保了M1的任何实现也是M[Lop 02]的实现由此，我们可以粗略地认为M是M1的重载.逻辑变量允许表达逻辑属性，这些属性涉及M中不直接存在的概念。这些变量也允许限制使用M1的操作.6.2应用于FWS在接口模块FWS ENV中，抽象变量是用于与环境通信的变量。其他变量是逻辑的：变量wp，se，wc逻辑变量Wp1，Wc2，Wc 1，Wc2，Wc 1，Wc2，Wc 2，Wc 2对应于FWS ENV的基本模块，即没有逻辑变量的FWS ENV是：机器FWS底座变量wp、se、wc初