可视化层次状态表示的事件B模型

可在www.sciencedirect.com在线获取理论计算机科学电子笔记280（2011）35-46www.elsevier.com/locate/entcs从事件B模型迪帕克湖Chaudhari1，2 Om P.Damani3印度理工学院计算机科学与工程系，孟买，印度孟买摘要一个系统的许多属性可能并不明显，只是通过快速检查相应的事件-B模型。用户通常依赖于动画、场景分析和状态转换图的检查用于发现系统的某些行为。我们提出了一种方法，用于生成可视化事件B模型的系统的层次表示。我们的表示是简洁的，它提供了多个视图，以帮助更好地理解Event-B模型。保留字：事件B，模型可视化，层次状态表示1引言在事件B中，系统的期望全局属性以不变量的形式指定，并且不变量保持证明确保这些属性在任何启用的事件执行后由系统维护[1]。但是，在执行启用的事件之后，接下来将启用或禁用哪些事件并不明显。用户通常依赖于动画、场景分析和状态转换图的检查来掌握系统的行为方面。ProB animator[9]在模型检查器的帮助下，可以生成B机状态空间的图形可视化。然而，由于ProB状态空间表示的非分层（non-hierarchical）性质，即使在采用状态空间缩减技术之后，降低状态空间图的复杂性也变得困难[10]。一般来说，分层状态转换图被发现在降低状态转换图的复杂性方面是有用的[6]。1这项工作得到了印度政府人力资源开发部和塔塔研究开发和设计中心（TRDDC）的部分支持。2 电子邮件地址：dipakc@cse.iitb.ac.in3 电子邮件地址：damani@cse.iitb.ac.in1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.01636D.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）35{1}|}{1}|}∈我们提出了一个分层表示，类似于状态图，可视化事件B模型。我们提出了一个自上而下的方法，直接从给定的事件B模型构建所需粒度的抽象表示。2分层抽象状态转移机为了表示离散事件系统，我们使用分层抽象状态转换机（HASTM）表示，该表示使用分层状态和保护转换的概念，类似于状态图[6]中的概念。在HASTM中，状态空间以树的形式排列（我们称之为状态-空间划分树），树的根节点表示所有有效状态系统，即，由所有不变量的结合所定义的状态。根节点根据某个谓词划分为子状态。子状态又使用适当的谓词进一步划分。图1示出了由我们的方法（ 算 法 1 ） 针 对 图 2 中 所 示 的 LiftEvent-B模型4生成的状态空间划分树，给定谓词（cf=topFloor）、（cf=botFloor）、（doorOpen=T），和（dirUp= T）。该算法从图1：Lift示例的状态空间划分树。层次关系用虚线箭头表示根节点，并在每个节点上选择一个分区谓词，该谓词使生成的HASTM中的转换数量最小化。这降低了生成的HASTM的复杂性。在划分树的同时，该算法还计算转换的前状态、转换保护和后状态（在2.1节中定义）。Lift模型的最终HASTM如图4所示。2.1HASTM的结构和语义如果v表示系统的变量，则集合Φ=v True是系统的整个状态空间。我们使用术语抽象状态来表示Φ的任何子集，而术语具体状态或只是状态来表示Φ的特定元素5抽象状态通常使用谓词来指定。如果Q（v）是一个在v中有自由变量的谓词，那么我们用Q表示满足Q（v）的所有具体状态的集合，即，Q=v Q（v）。 如果一个系统处于一个具体的状态q， 抽象状态，则系统被称为处于抽象状态Q。HASTM是元组H=H，S，>，T，t，0，其中4Lift Event-B模型改编自ProB工具附带的B模型[9]。5.术语抽象状态和具体状态不应与术语抽象模型和具体状态混淆。具体模型，用于改进。INVdoor_open=Tcf top地板cf=顶层dir_up=Tdir_up=Fdoor_open=Fcf > botFloorcf=botFloorD.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）3537>W公司简介HS S P·∈ ∈ S>·∈ S\{H} ∈ SH∈>>·∈ SH·S>铝合金>S常数：变数：底部地板，顶部地板PushCallBtn=任何F在哪里公理：cf、doorOpen、callbtns、DirUpf∈ topF地板.. botF地板^当移动到上=dirUp=T^ReverseUp=当dirUp=Ff∈/callbtnsdoorOpen=FdoorOpen=FbotF loor∈Z，topF loor∈Z然后F=cf上请求的cftopF地板已请求^botF地板topF地板下载请求不变量：callbtns：=callbtns{f}然后cf∈/callbtnscf∈/callbtns电话号码doorOpen∈BOOL端OpenDoor=cf：=cf+1然后dirUp：=T（botF floor.. topF地板）当doorOpen=F^端向下移动=端dirUp∈BOOL（doorOpen=T）然后cf∈callbtns当door打开：=TdirUp=FdoorOpen=F^反向向下=当dirUp=TdoorOpen=FInit=（cf∈callbtns）贝吉恩^端关门=downRequestedcf > botFloor已申请^cf：=底部地板当door打开：=Fdoor打开=TdirUp：=T端callbtns：=callbtns然后，door打开：=F下载请求然后cf∈/callbtnscf：=cf− 1然后cf∈/callbtnsdirUp：=F电话号码：端端端callbtns\{cf}图二、电梯控制器的事件B模型 upRequested表示“请求”。（c ∈ Z c> cf c ∈ callbtns），downRequested代表c。（c∈Z<$c cf<$c∈callbtns），T代表True，F代表False。• v表示系统的变量。•是抽象状态的有限集合其中Φ是系统所有状态的集合。•是上的一个层次关系，满足以下条件对于任意两个抽象状态X和Y，X Y X Y。存在唯一的抽象状态r，称为的根状态，记作root（），使得r / ran（），其中ran（）是关系的值域。对于每个X根（），则存在唯一的抽象状态Y等这个Y X。Y被称为X的直接超态，而X被称为Y的直接子态。没有任何直接子状态的抽象状态称为基本抽象状态。如果X是中的非基本抽象状态，并且是X的所有直接子状态的集合，则划分集合X。也就是说，X的所有直接子状态是共同穷举的（（W）= X），并且X的任何两个不同的直接子状态是互斥的。（<$A<$B）.A∈ W <$B∈ W<$A=B<$A<$B=<$）• 表示事件签名集。事件签名由事件名称和事件参数组成。• T是一个5元转换关系。 T的每一个元素都代表一个跃迁。我们将5元组t的元素称为t.Evt、t.P re、t.K、t.Act和t.P ost，其中t.Evt是事件签名，t.P re是转换的前状态（原始抽象状态），t.K（v，u）是转换保护谓词（其中u是t.Evt的事件参数），t.P ost∈ S是后状态（目标抽象38D.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）35⟨⟩t.Pre·−→{}|HHH状态），而t.Act是事件t.Evt .的转换动作。转移作用是对系统变量的同时赋值。·对于任意两个转换t1和t2，如果t1.Evt=t2.Evt，则t1.Pre（v）t1.K（v，u）<$（t2.Pre（v）t2.K（v，u））（1）其中u是事件t1.Evt（和t2.Evt）的参数。在本小节的结尾给出了这种情况的动机•t0是一个5元组t0.Evt，t0.Pre，t0.K，t0.Act，t0.Post，表示初始化转换，其中t0.Evt是初始化事件，t0.Pre是一个伪状态，表示t0的前状态，转换保护t0.K是True，Act0是初始化动作，S0∈ S是初始抽象状态.转换t表示为{t.Pret.Evt（u）[t.K（v，u）]/t.Actt. Post}，其中u是Evt的参数。如果系统是i}n-t-h-e-a-b-s-t-ra-c-t-s-t-a-te-→{并且满足转换保护t K（v，u），则转换t被称为被使能。只有在启用时才能进行转换。如果转换t被启用并且它发生，则在执行t.Act之后，系统移动到抽象状态t. Post。HASTM中转换的这种行为语义在下面的证明义务中被捕获。t.P re（v）t.K（v，u）BA（v，u，vJ）t.P ost（vJ）其中BA（v，u，vJ）是动作t.Act的前后谓词。初始转换将系统转换为初始抽象状态S0，并表示为init[True]/Act0J JS0。初始化转换的证明义务是A（v）S0（v），其中A是动作Act0的后谓词。HASTM定义中的等式1中的条件确保对于给定的状态和事件参数，不启用对应于同一事件的2.2将Event-B机器表示为HASTM设M是一个事件B机器，v是它的变量，I（v）是它的不变量。 设Em是由“任何u，其中G m（v，u）则v：BA m（v，u，v j）结束“表示的事件，设A（vJ）为init事件的after谓词。(We从[1]中调整符号HASTMH：v，S，>，，T，t0是事件B机器M的表示，如果(i) 变量v和事件签名M中的变量和事件签名与M中的变量和事件签名相同。(ii) 根（H）惠I（v）。(iii) 对于任何转移tin，动作t.Act与事件t.Evt在M中的动作相同。 中的init转换操作与M中的init事件操作相同。(iv) 设t1，t2，.. . ，t，k是对应于M中的事件E，m的H中的转变D.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）3539H∧⇒H∧ ∧ ¬−→{}{}−→{}(i.e. t i.Evt=E mfor i ∈ 1. k）然后I（v）Gm（v，u）惠i ∈1.. K（ti.Pre（v）ti.K（v，u））（2）等式2中的条件连同等式1中的条件意味着当且仅当存在单个启用的转变tin，其中t=Gm时，在M中启用事件Gm。HASTM表示用于Event-B细化链中的特定Event-B模型。细化链中的每个Event-B模型都有一个单独的HASTM表示。在这项工作中，我们没有建立一个链接之间的HASTM表示对应于抽象和具体的事件B模型。3从Event-B机我们首先解释了交互式生成HASTM的过程，然后给出了一个从给定的Event-B机器自动生成HASTM的算法。设t是中的一个跃迁，X是t的一个子态。如果t.P re（v），则转换t被称为在X中独占地启用t.K（v，u）X（v）其中u是参数 的t.Evt.考虑转换t：{t.Pret.Evt（u）[t.K（v，u）]/t.Actt. Post}在H. 第-用谓词p（v）ge}ne−r−a−te−s−−tw−−o−i−m−−ed−i−a→te{t.Pre的子状态，即X1：t.P re（v）p（v）和X2：t. Pre（v）p（v）. 如果t在以下两种情况中独占启用，X1或X2，则称t服从t. Pre关于p（v）的3.1HASTM的交互式生成我们 首先定义 了一个事 件B机器 的原始HASTM 表示 ，它是一 个非常简 单的HASTM，只有一个抽象状态I。考虑2.2节中描述的事件B机器M。设r为M中事件的个数。M的原始HASTM是具有与M相同的变量和事件签名的HASTM，单个抽象状态I和以下转换。init[T rue]/Act0Ei[Gi]/ActiI和II表示i从1到r。原始HASTM中所有变迁的证明义务与M.很容易验证M的原始HASTM满足2.2节中提到的条件，因此代表M。为了生成所需粒度的HASTM，我们从给定Event-B机器的原始HASTM开始，然后依次划分基本抽象状态并根据以下过程修改转换用于划分基本抽象状态的过程X.(i) 划分：选择一个划分谓词p（v），将抽象状态X划分为两个子状态X1：X（v）p（v）和X2：X（v）<$p（v）。40D.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）35E（u）[K（v，u）]/Act}−→{{ }−→{}YY^(ii) 修改预状态：对于任何转换t：{XE（u）[K（v，u）]/Act. 从X开始，有两个可能性}−→{(a) t在X1中独占地启用：在这种情况下，我们将t的预状态加强为X1。 如果转换保护K（v，u）具有p（v）作为合取，则移除它来自K（v，u），因为它现在是冗余的，因为X1已经有合取。转换现在变为t：{X1E（u）[KJ（v，u）]/Act. 其中，KJ（v，u）是{1}从K（v，u）中取出vi}ng−−t−h−e−c−o−n−j−u−n−c→tp（v）后得到的谓词。(b) t在X2中独占地启用：这种情况与情况a对称。(c) t在X 1和X 2中都没有被独占地启用：在这种情况下，我们有两个选择。• 在过渡{X}−−−−−−−→{。}，创建两个新的transi-选项：{X1E（u）[K（v，u）]/Act. }和{X2E（u）[K（v，u）]/Act. }}−→{E（u）[K（v，u）]/Act• 保持转换为X。 . 这 是 自 动 HASTM生成算法中的默认选项（将在3.2节中讨论）。我们在算法1中选择此选项以防止过渡的数量增加。(iii) 加强后状态：加强所有被检查的转换的后状态（其前状态在步骤c中已经改变的转换和其后状态在步骤i中已经被划分的转换）。考虑转换t：{.E（u）[K（v，u）]/ActY}，其后状态为Y。设YJbe直接子状态}e−o−f−−t−h−a−t−a−lr−e→ad{y存在于状态空间部分中树 如果证明义务为{E（u）[K（v，u）]/ActYJ}被放电，则加强tr}a n−s−it−i−o−n−t−o−J−的p态。→N{ow，其中YJ为新的后状态，重复上述步骤，直至证明义务不能履行或达到基本抽象状态。该算法在算法1中的函数strengthenPostState中给出。范例：考虑图2中给出的Lift Event-B模型。我们从一个原始的HASTM具有单个抽象状态I，转换：{IEi[Gi]/ActiI}对于i从1到7，以及init转换init[True]/Act0}−→{I}。不变量I和事件如图2所示。−→{我们现在展示对应于MoveUp和CloseDoor在根抽象状态I分区后被修改。• 我们使用谓词p=（dirU p=T）将抽象状态I划分为两个直接子状态（Ip）和（Ip）。• 考虑原始HASTM中对应于事件MoveU p的转变。MoveUp（dirUp=T）（cf∈/callbtn）upReuested/cf：=cf+1{I}（cftopF floor）门打开=F<−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−→{I}由于原始HASTM具有单个抽象状态I，预状态以及D.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）3541∧∧∧联系我们联系我们}-→{}{I}转 换 后 的 状 态 是 I 。 预 状 态 I 和 转 换 保 护 意 味 着 （ dirUp=T ） ， 因 此 I（dirUp=T）。这种转换在I（dirUp=T）中是唯一启用的，因此可以用谓词（dirUp=T）对抽象状态I进行划分。按照步骤a，我们加强了转换到I的前状态（dirUp = T），并通过删除合取（dirUp=T）来削弱转换保护。修改后的过渡是{I=T（dirUp）}（cf∈/callbtn）最后一个问题（cftopF floor）门打开=F个文件夹阿吉夫¬∧⇒>联系我们›→}INVdirUp=TdirUp=F图三.使用分区谓词（dirUp=T）交互生成的Lift Event-B机器的HASTM表示。全局变量：输入变量：M：事件B机器，具有r个事件输出：HASTMH=V，S，>，V，T，t0VP：分割谓词functionMain（）BuildPrimitive HASTM（）PartitionAbstractState（I）for transitiont inTStrengthenPostState（t）StrengthenPostState（t0）函数BuildPrimitiveHASTM（）v：=M的变量函数SelectPredicate（X：abstract state）评分：=//score P N对于P中的P如果X（v）已经共轭p（v）或p（v）继续：=t.Pre=X且t服从于X与pM：=M的事件签名I：=M的不变量的合取S：={I}评分（p）：=eT如果得分=返回Null：=：={Ev：Em，Pre：I，K：Gm，Act：Actm，Post：I|m∈ 1..r}t0：=Evt：init，Pre：，bestP red：如果score（bestP red）= 0，则argma xpscore（p）bestP red：=0返回bestP红色functionstrengthenPostState（t：transition）功能K：T rue，Act：Act0，Post：IPartitionAbstractState（X：=Y t.Post YY=0 //t.Post是一个基本的抽象状态抽象状态）p：=SelectPredicate（X）ifp=0返回返回第二节债务人的责任X1：= AddSubState（X，p）t.Evt[t.K]/t.Act{t.Pre}−−→{Y}X2：= AddSubState（X，p）PartitionAbstractState（X1）PartitionAbstractState（X2）函数AddSubState（X：抽象状态，q：同品种器械）XJ（v）：=X（v）<$q（v）排出t.Post：=YstrengthenPostState（t）break返回S：=S <${XJ}J：=X X对于T中的t，使得t.Pre=X如果（X（v））t.K（v，u）q（v））t.Pre：=XJt.K = KJ其中KJ是从t.K中移除共轭q（v）（如果它存在的话）之后获得的谓词。为ΣD.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）3543returnXJ算法1. 给定一组划分谓词，从Event-B机器生成HASTM表示的算法。44D.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）35<$→}联系我们分区谓词是从给定的谓词集合中自动选择的。我们从M的原始HASTM开始，然后递归地划分抽象状态I。在状态空间划分树中的每个基本抽象状态处，选择进一步的划分谓词以最大化服从于用所选择的谓词划分的事件的数量这使我们能够加强这些事件的预状态，而不会增加生成的HASTM中的转换数量。我们定义了一个得分函数，它为每个划分谓词p分配了适合用p划分X的转换数 （ 参 见 算 法 1 中 的 函 数 SelectPredicate ） 。 图 4 显 示 了 给 定 分 区 谓 词（cf=topFloor）、（cf=botF loor）、（doorOpen=T）和（dirUp=T）的情况下，算法1生成的Lift Event-B机器的HASTM表示。抽象状态I的得分函数是score=（doorOpen=T）6，（dirUp=T）4，（cf=topFloor）2，（cf=botF floor）2 .我们选择具有最大得分的谓词（doorOpen = T）来划分抽象状态I。 我们对子状态重复这个过程，直到所有谓词都被利用，同时创建抽象状态或所有给定谓词的得分为零。对于所选择的划分谓词，如果存在不服从划分的事件，则我们决定不加强预状态。根据HASTM的定义，此选择不是必需的。但是，我们在自动生成算法中选择此选项，以防止过渡的数量增加。用于划分和预状态增强的过程在算法1中的函数PartitionAbstractState和AddSubState中实现。由算法1生成的HASTM中的转换数量始终等于事件B模型中的事件数量在完整的状态划分树准备就绪并且所有转换的前状态被加强为适当的抽象状态之后 ， 我 们 加 强 所 有 转 换 的 后 状 态 。 有 关 详 细 信 息 ， 请 参 阅 算 法 1 中 的 函 数StrengthenPostState在HASTM自动生成后，用户可以通过交互式算法进一步修改表示，用不同的谓词划分基本状态。3.3多个视图在图4所示的HASTM中，自动HASTM生成算法没有划分节点（doorOpen=T），因为所有谓词的得分都为零。使用任何给定的谓词进行分区都不允许我们在不拆分CloseDoor转换的情况下增强它的预状态虽 然 自 动 生 成 算 法 避 免 了 为 单 个 事 件 生 成 多 个 例 如 ， 在 图 4 中 的 节 点（dirUp=T）处，如果我们选择谓词（cf=botFloor）而不是（cf=topFloor），则会得到图5所示的不同表示。这种划分增加了HASTM表示的复杂性，因为为MoveUp事件生成了两个转换。然而，这有时是可取的，因为多个HASTMD.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）3545INVdoor打开=TdoorOpen=FdirUp = TdirUp = Fcf=顶层cf > botFloorcf top地板cf = botFloor图四、 给定划分谓词（cf = topF loor）、（cf = botF loor）、（doorOpen = T）和（dirUp = T），由算法1生成的Lift Event-B机器的HASTM表示。图五.提升事件-B机器的替代HASTM表示。在节点（dirUp=T），我们交互式地选择划分谓词（cf=botFloor）。图中没有显示转换保护和操作，所有事件都与图4中的相同这些表示突出了系统的不同方面。从图4中注意到，在执行OpenDoor事件之后，除了CloseDoor和PushCallBtn之外的所有其他事件都被禁用。 此属性可能无法从Event-B计算机中清除。 当（cf= topFloor）未从Event-B模型中清除时禁用ReverseUp事件的另一个属性。ReverseUp事件的保护与不变量一起暗示（cf botFloorcf=顶层反向向下dirUp = Fcf=顶层下移cf top地板上移cf top地板cf>botFloor下移反向向下Init上移cf=botFloorReverseUpcf=botFloorReverseUpPushCallBtn46D.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）35用于对需要事件顺序排序的问题进行建模。在这项工作中提出的对于这样的模型，涉及程序计数器的谓词是分区谓词的自然选择。虽然，在本文中，我们只考虑二进制分区的状态空间，该方法可以很容易地扩展到多进制分区。在[7]中，提出了三种基于动画和证明的构造状态转移图的技术.这项工作建议将图的状态与抽象不变量相关联，以减少状态的数量，有限的一个。 ProB工具[9]可以生成B机的状态空间图通过遍历机器的状态空间。然而，对于大多数模型，完整的状态空间没有被探索。此外，对于更大的状态空间，这些图变得非常复杂。在[10]中，提出了两种用于降低状态空间图的复杂性的算法，使得可以可视化更大的状态空间。然而，状态空间图中的转换没有用谓词标记。在文献[2]中，我们从Event-B模型中导出了一个隐式算法结构的隐式图。流图不使用分层状态，并且随着模型中事件数量的增加会变得非常复杂。在HASTM中，表示的复杂性可以通过分层抽象状态的选择性划分来保持在可理解的水平然而，有时候获得正确的透视图可能需要人工干预来选择正确的划分谓词。[3，4]中的工作提出了一种方法和工具（GeneSyst），用于从事件B规范构建符号标记的转换系统。GeneSyst系统要求与转换系统中的状态相关联的不变量被指定由用户GeneSyst系统支持模型的改进。HASTM具有层次化的状态，但需要更多的工作来建立对应于细化链中抽象和具体Event-B模型的在这项工作中，我们划分的全局状态空间的Event-B机。 我们想探索由事件参数定义的局部状态空间的划分。在开发了HASTM的基本概念和从事件B模型自动生成HASTM的算法之后，我们现在计划实现该算法，并在各种事件上尝试这种可视化技术B型。5结论在这项工作中，我们提出了一种方法，通过使用层次状态转换机（HASTM）可视化事件B模型。我们指定了HASTM应该满足的条件，以表示事件B机器。然后，我们提出了一个算法自动生成的HASTM表示从一个给定的事件B模型和一组分区谓词。借助实例，我们证明了多个HASTM表示有助于掌握某些特定的知识，D.L. Chaudhari，O.P.Damani/Electronic Notes in Theoretical Computer Science 280（2011）3547制度的道德方面引用[1] 让·雷蒙德·阿布里尔事件B建模：系统与软件工程。剑桥大学出版社，剑桥，纽约，2010年。[2] Jens Bendisposto和Michael Leuschel。事件B的自动流程分析。Dimitra Giannakopoulou和FernandoOrejas，编辑， 软件工程的基本方法，计算机科学讲义第6603卷，第 50-64页。Springer Berlin/Heidelberg，2011. 10.1007/978-3-642-19811-3_5。[3] 迪迪埃·伯特和弗朗西斯·凯夫从B抽象系统构造有限标号迁移系统在第二届国际综合形式方法会议论文集，IFM'00，第235-254页，伦敦，英国，2000年。史普林格出版社[4] Didier Bert，Marie-Laure Potet和Nicolas Stouls。GeneSyst：一个推理B事件规范行为方面的工具适用于安全属性。CoRR，abs/1004.1472，2010年。[5] 斯特凡·哈勒斯泰德结构化事件B模型和证明。In Marc Frappier，Uwe Glässer，Sarfraz Khurshid，Régine Laleau，and Steve Reeves，editors，Abstract State Machines，Alloy，B and Z，volume 5977ofLecture Notes in Computer Science，pages 273-286. Springer Berlin/ Heidelberg，2010. 10.1007/978-3-642-11811-1_21。[6] 大卫·哈雷尔。状态图：复杂系统的可视化形式。Science of Computer Programming，8（3）：231[7] A. Idani和Y.勒杜来自正式B规范的动态图形化UML视图。信息与软件技术，48（3）：154[8] 洪乐当和珍宁·苏奎埃对B语言中UML状态图建模的贡献。在第三届国际综合形式方法会议论文集，IFM'02，第109-127页，伦敦，英国，英国，2002年。史普林格出版社[9] 迈克尔·鲁舍尔和迈克尔·巴特勒。ProB：B的模型检查器。 FME 2003：正式方法，LNCS 2805，第855-874页。Springer-Verlag，2003.[10] 迈克尔·鲁舍尔和艾德·特纳。在pro B中可视化更大的状态空间。在ZB 2005：Formal Specificationand Development in Z and B，卷3455的Lecture Notes in Computer Science ，第6-23页。SpringerBerlin/ Heidelberg，2005.[11] Emil Sekerinski和Ra fik Zurob。将状态图转换为B。在Proc. of the 3rd International Conference onIntegrated Formal Methods（IFMSpringer-Verlag，2002.[12] 科林·斯努克和迈克尔·巴特勒。 UML-B：UML辅助的形式化建模与设计。ACM Transactions onSoftware Engineering and Methodology，15（1）：92-122，2006。[13] 科林·斯努克和迈克尔·巴特勒。UML-B和Event-B：语言和工具的集成。在IASTED软件工程国际会议论文集，SE'08，第336-341页，Anaheim，CA，USA，2008年。Press.