文摘

事件b是一种正式的建模语言,非常适用于软件工程,但它缺乏建模时的能力。研究人员已经提出了一些方法建模时间限制在事件b。现有方法的局限性,首先,现有的研究缺乏一个系统的细化框架基于事件b;其次,现有的方法只有在事件b模型时间框架,不能顺利转化为automata-based模型时间自动机等促进时间属性的验证。这些限制使其更难以与事件b模型和验证实时系统,因为它是非常耗时的事件b证明时间属性框架。在本文中,我们首先提出了一个系统的细化框架来表达和精炼时间约束事件b。其次,我们也提出了各种垂直细分模式和水平扩展模式指导建模者逐步完善事件b实时模型。最后,我们使用一个实时系统演示我们的方法的实用性。实验结果表明,该方法可以使事件b更方便的实时系统建模和模型更容易转换为时间自动机模型,从而促进各种时间属性的验证。

1。介绍

实时并发系统的复杂性使得工程师有必要使用正式的方法模型和验证系统。正式的方法使研究人员能够使用严格的数学模型来描述系统需求和系统行为和验证给定的系统或系统模型是否符合所需的所有属性。事件b (1]是一种正式的语言,是最接近目前软件工程,非常适合建模实时并发系统的行为。逐步完善框架和自动代码生成功能的事件b不仅确保模型的正确性和一致性,还提供良好的软件工程支持。然而,事件b本身不支持时间的建模,和它的表达能力有一些局限性;因此很难事件b来验证实时系统的时间特性。

为了使用事件b模型和验证实时系统,做的工作人员包括以下:第一个方向是使用事件b本身的功能模型,通常建模离散时钟定时使用“tick_tock”事件以及建模各种时间模式;另一个方向是翻译事件b模型可核查的时间模型,如UPPAAL模型,然后验证其TCTL属性。

上述时间建模的研究已经解决了一些问题事件b。然而,这些作品仍然有一些问题:第一,目前的工作缺乏系统性和全面优化框架。他们已经解决了的问题是具体和详细的问题。其次,尽管有一些方法可以系统地事件b模型时间框架,它们使时间属性更加困难和繁琐的证明,。根据的观点多米尼克•Cansell et al。2],它是非常困难和耗时的验证时间事件b模型中的属性。第三,存在一些问题翻译事件b模型UPPAAL直接时间自动机,因为许多语法元素事件b的建模语言,它是基于一阶谓词逻辑不能直接转换成时间自动机。

简而言之,目前正式的实时系统建模和验证工作事件b提出这样的要求:首先,我们需要一个框架,支持自顶向下的建模和优化过程。其次,我们需要一个“中间模型”,使翻译过程从事件b时间自动机“平滑”支持的验证时间事件b模型的属性。

的发明iUML-B状态机(3)使研究人员能够描述事件b模型的逐步求精过程直观和视觉方式。它还使我们能够以图形的方式表达事件b的时间间隔。我们可以用iUML-B状态机来“模仿”时间自动机的行为模式,这样人们可以很容易地将iUML-B状态机转化为相应的时间自动机模型和验证的时间属性事件b模型更容易。

“时间自动机的模式”(4盾也启示我们提出的方法。根据他的经验建模实时系统,董提出了超过12个时间自动机的模式,这代表了实时系统建模时常见问题。我们介绍了侗族的想法到事件b iUML-B建模框架和使用状态机来表达各种时间自动机模式支持实时系统的建模和验证事件b。

本文的贡献包括以下几点:首先,我们提出了一个时间事件b模型的细化框架基于iUML-B状态机。它提供了一个指导框架建模实时系统使用事件b。其次,我们提出了“垂直细分模式”和“横向细分模式”董提出的基于时间自动机的模式。这些模式可以帮助modeler快速构建一个实时事件b模型。第三,我们提出的概念iUML-B功能状态机和iUML-B时钟状态机模型不计时的部分和定时系统的一部分,分别。最后,我们建模起搏器系统使用我们的方法相比,我们的方法与现有的实时事件b方法。

本文的其余部分安排如下:在部分2,我们介绍了各种方法来建模实时系统和验证使用事件b和其他形式。节3,我们介绍了本文所必需的基本知识,包括事件b的引入,iUML-B状态机,时间自动机的定义和时间自动机的模式。部分4本文的方法论框架细节,包括各种iUML-B模式对应于不同的时间自动机状态机模式基于我们提出的方法。节5,我们使用本文提出的框架来构建一个实时的起搏器模型系统。本文的方法评价部分6。节7,我们结束我们的工作。

2。相关的工作

正如我们所提到的部分1,有两个主要方向在实时系统建模和验证使用事件b。研究人员已经做了一些工作在使用事件b本身来建模实时系统。巴特勒和Falampin5)首次提出一个方法在经典模型离散b .这种方法使用一个自然数变量(名为时钟变量)来表示当前时间和表达时间的推移增加这个变量的值。巴特勒的最大区别的方法和经典的时间前方法建模方法是,如果当前时间等于一个最后期限,某些操作是用来防止时间的推移。这个想法已经通过所有后续类似的作品包括我们的方法。Cansell [2)首次提出“时间约束模式”的概念,用“tick_tock”事件来表达时间的推移。随后,官尤里斯Rehm [6- - - - - -8)提出了“过程模式”来表达两个事件之间的时间间隔,这使人们能够模型和理性事件b的实时性能。Sarshogh [9,10)提出了一个名为“时间属性”的方法,其中包括三个时间模式:延迟模式,失效模式,截止日期模式。这些模式是用来表达延迟的概念,超时,实时系统的最后期限。Sulskus [11,12)提出了一个基于Sarshogha时间间隔方法的工作。的时间间隔方法iUML-B状态机的状态节点代表的时间间隔和使用输入和输出状态节点的边代表触发事件和响应事件的时间间隔,分别。上述方法是非常有用的对于建模系统的实时性能,但是仍然需要时间验证的属性启发式证明的定理证明框架。因此,正如我们所提到的部分1,这地方一个伟大的研究模型和验证系统的负担。

另一个方向的建模和验证使用事件b实时系统是将事件b模型转化为一个UPPAAL时间自动机。例如,阿列克谢Iliasov [13]提出了一种方法翻译事件b模型时间自动机模型,使用流程视图之间的中间表示语言事件b模型和UPPAAL模型。这种方法的局限性是它需要从事件b模型提取流程视图之前翻译。想把它们做为虚荣和Jesper停泊et al。14- - - - - -16)也提出了一个时间细化框架,支持Correct-By-Construction方法综合事件b和UPPAAL时间自动机。他们的方法始于一个简单的事件b模型及其相应的UPPAAL时间自动机。细化后的事件b模型和一致性的证明,事件b模型转化为相应的时间自动机模型,和验证的时间属性在UPPAAL环境中执行。最终的模型(包括事件b模型和时间自动机模型)系统的逐渐采用这种迭代过程。这种方法的优点是,它不需要任何修改事件b模型和时间自动机模型,也不需要学习新的正式系统。这种方法的缺点是,许多元素事件b建模语言是基于一阶谓词逻辑,不能直接转换成时间自动机。

3所示。初步

3.1。事件b和iUML-B状态机

3.1.1。事件b

事件b是一个基于事件的正式的建模语言,使用它的第一个类对象的事件。事件的一般形式如下:

e≙当保安行动结束

一个事件由警卫和行动。一个事件e启用时,所有的警卫都满意,和行动表达事件的影响e,也就是说,变量的修改。事件b使用变量来表达系统的状态和改变这些国家用行动在事件。

3.1.2。iUML-B状态机及其改进

c·斯努克发明UML-B [17),一个“类似于uml”图形化前端事件b。UML-B使用类图和状态图熟悉软件工程师,系统工程师模型系统。UML-B表达的系统模型可以生成相应的事件b代码直接在罗丹的平台。最近,UML-B已经演变成iUML-B(集成UML-B),允许UML-B类图和状态图直接嵌入到一个事件b机。iUML-B已成功应用于一些大型项目在欧洲委员会,如(3,18]。

尽管UML-B最初是作为UML概要文件(17)实现翻译从UML类图和状态图到B“经典”,它已经演变为一个独立的正式定义建模语言自斯努克UML-B元模型(19]。从那时起,UML-B模型的分解和细化过程对应的分解和细化过程事件b模型,而不是定义的UML模型的分解和细化对象管理组织(OMG)。

国家之间的差异的UML和UML-B分解分解UML-B需要遵循很多约束。此外,建模者必须证明抽象模型之间的一致性和改进模型。说(20.- - - - - -23)提出了许多国家UML-B细化规则,这是各种细化研究的基础。说的工作的支持,UML-B模型的分解和细化必须遵循一定的正式规则,和一些证明义务iUML-B (PO)自动生成的插件必须“排放”(即。被证明),以确保抽象模型之间的一致性和具体细化模型;否则,细化过程不能继续。

3.2。时间自动机和时间自动机的模式

3.2.1之上。时间自动机及其定义

时间自动机是一个有限状态机和一个时钟。它非常适合建模实时系统的行为和验证的时间属性。它提供了一个通用的方法,来注释状态转换图时间限制使用有限数量的时钟变量。在时间自动机的正式系统中,每个组件或子系统所描述的一组节点代表系统的状态。定向节点之间的边表示状态转换,定向边缘上的标志代表的名字事件触发的过渡。时间自动机的状态可以表达一个瞬时状态或时期。研究人员开发和深入研究使用时间自动机的方法检查安全和进步系统的属性。有许多支持时间自动机的分析和验证工具,如UPPAAL [24),科隆诺斯(25),和调度性分析仪(26]。

定义1。一个时间自动机一个被定义为一个=(l,初始化,FΣ,C,发票,T),(我)l是一组有限状态(2)初始化∈l代表了初始状态(3)F终端状态设置吗(iv)Σ/事件是一组动作(v)C一组有限的时钟吗(vi)发票定义了一组局部不变量;这将给各州约束(七)T表示一组转换关系,表示为l×Σ×2^C×Φ(C)×l,Φ(C)是一组时钟约束,定义为以下语法(x是一个时钟;c是一个实数):φ:= true |x≤c|c≤x|x<c|c<x|φ₁∧φ₂

3.2.2。时间自动机的模式

时间自动机的模式(4,27,28)是一组可重用和可组合正式董提出的模型。它的目标是用这些简单的构成模型来建模实时系统和验证效率。这些模式,如延迟,定时中断,最后期限,和超时是抽象的常见的并发和分布式实时系统的概念和现象。时间自动机的模式,时间自动机被抽象为一个三角形。左顶点或圆连接到左顶点代表了时间自动机的初始状态;右边代表其最终状态。图1显示最后期限时间自动机的模式。

我们董提出的时间自动机的模式进行分类,把它们分成垂直细分模式和横向扩张模式。区分这两种模式的原则是否有超过一个时间自动机的模式。这些模式,只有添加新的州一个时间自动机被归类为垂直细分模式,而代表多个时间自动机(即之间的关系。,有一个以上的时间自动机的模式)被列为一个水平扩张模式。此外,我们还提出了三个新的垂直细分模式表达原子态的概念抽象的时间自动机进一步分解为多个时间段。因此,这项工作的基础上,我们进一步将垂直细分模式分为两类:第一类被称为增量改进模式,这是那些添加新的状态或转换时间自动机。第二种类型叫做分解细化模式,是将某一原子态的时间自动机分解为多个新的原子状态。时间自动机模式的分类和汇总如表所示1,三个新提出的分解模式标记为斜体。

我们使用一个或一个_我代表一个单一的时间自动机在所有时间自动机的模式定义。由于空间限制,我们只使用三个典型的例子,即截止日期模式,序列模式,和事件中断模式来说明这三种类型的优化模式,分别。

3.2.3。垂直细分模式

逐步求精模式的例子:截止日期模式。最后期限模式用于模型最后期限的实时系统的概念,如图1。的执行时间自动机内必须完成t时间单位。因此,所有州一个标注是不变的吗x≤t(x是一个时钟变量)。当系统进入自动机一个,时钟x复位为0。最后期限模式的正式定义如下。

定义2。的最后期限(一个,t)≝(l,初始化,FΣ,C,发票,T),
l≜l_一个∪{l₀},初始化≜l₀,F≜F_一个,Σ≜Σ_一个,C≜C_一个∪{x},
发票≜{(l₀(紧急)}∪{l,发票)|l∈l∧发票= (发票(l∧)x≤t)},
T≜T_一个∪{(l₀,τ,{x},真正的,l₁)}
分解细化模式的例子:序列分解模式。序列分解模式分解原子状态的时间自动机为多个顺序亚态。此模式用于分解抽象为多个小区间的时间间隔,如图2。图中的虚线框代表了原子态节点分解之前,被称为父状态;在分解后的虚线框代表了儿童心理状态。每个孩子必须在有限的时间内完成其执行状态,和所有的子状态的执行时间之和不能超过其父状态的时间限制。序列模式的正式定义如下。

定义3。Seq(一个,t,t₃,t₄,t₅)≝(l,初始化,FΣ,C,发票,T),
l≜l_一个∪{l₃,l₄,l₅}\ {l},初始化≜l₁,F≜F_一个,Σ≜Σ_一个∪{一个₂,一个₃},C≜C_一个∪{x₃,x₄,x₅},
发票≜{(l₃,x₃≤t₃),(l₄,x₄≤t₄),(l₅,x₅≤t₅)}∪发票_一个。
T≜T_一个∪{(l₂,一个₁,{x₃},真的,l₃)}∪{(l₃,一个₂,{x₄},x₃>t₃。,l₄)}
∪{(l₄,一个₃,{x₅},x₄>t₄,l₅)}∪{(l₅,一个₄,∅,x₅>t₅,l₆)}\ {(l₂,一个₁,{x},真正的,l)}
\ {(l,一个₄,∅,x>t,l₆)}

3.2.4。横向扩张模式

事件中断模式。基于事件的中断事件中断模式用于模型,如图3。当一个事件一个发生,不管什么时间自动机的状态一个₁,它将转移到时间自动机吗一个₂来执行。事件的正式定义中断模式如下。

定义4。中断(一个₁,一个₂,一个)≝(l,初始化,FΣ,C,发票,T),
l≜l₁∪l₂,初始化≜l₁,F≜F₁∪F₂,Σ≜Σ₁∪Σ₂∪{一个},C≜C₁∪C₂,
发票≜发票₁∪发票₂,
T≜T₁∪T₂∪{(l,,{x},真正的,l₂)l |∈l₁}

4所示。方法

4.1。事件b的时间优化框架的概述

在本节中,我们使用了iUML-B状态机来表达时间的推移,时间间隔的分解,和多个并发实时对象的行为约束。我们将实时系统的控制流模型分为两类根据时间自动机理论的方法:(我)功能模型:这是“不计时的控制流模型在不增加时间限制。应该强调,我们规定,每个功能状态机描述一个变量的状态转换。这个想法来自于“原子状态机”提出了我们的以前的工作29日,30.]。(2)时间推移模型:在实时系统中,时间的推移也是一个重要因素影响的事件序列的系统,所以有必要模型具体时间的推移。

我们使用“功能状态机”和“股票状态机”来表达这两个上述模型,分别。(1)功能状态机:它是用来表达系统的“不计时的”行为。这种方法通常用于时间自动机的研究。它只表达系统中的一系列事件没有时间限制,没有时间限制的控制流。我们使用了“链接”能力建设iUML-B状态机的状态机的功能;即过渡的边缘iUML-B状态机可以与现有的“链接”事件b模型中的事件,并自动生成的代码嵌入到上下文(集、常数和公理)和机器(变量、事件和不变量)来控制这些事件的顺序。例如,假设我们已经写了五事件:“初始化”,e₁”、“e₂”、“e₃”和“e₄,“如果我们想要控制这些事件的顺序,初始化- >e₁- >e₂- >e₃- >e₄,“- >”意味着事件在其左边必须对发生在活动之前,我们可以创建一个iUML-B状态机和“链接”这五个事件的边缘过渡状态机,如图4。斜体的代码如图4由iUML-B代码自动生成状态机控制事件的顺序。(2)股票状态机:这是用来表达时间的推移,包括全球时钟的流逝以及本地时钟的增量和复位。股票行情自动收录器状态机的一个例子是图的左上角所示5。它只有一个事件蜱虫,用于增加全局时钟变量的值和本地时钟变量。

通过这种方式,我们可以“模仿”的时间自动机的组合功能状态机和股票状态机。假设有一个醒目的状态机TickerStm和功能状态机FunctionStm和“⊗”用于表示状态机的组成;然后TickerStm⊗FunctionStm可以用来表示事件b码产生的这两个状态机。使用功能状态机的组成和股票状态机,我们可以得到一个等价的模型类似于时间自动机事件b(我们把它命名为“原子时间状态机”,尽管它是不可见的),如图5。

我们使用图6施工过程的详细解释功能状态机和时钟状态机。为了表达我们的方法的意思很明显,在几家大型的数据在这一节中,我们只使用一个稳定的圆形符号与数字或字母来表达iUML-B状态机的状态节点,用虚线圆角矩形表示iUML-B状态机的超级大国,也就是说,那些含有亚态的状态。例如,国家“0”和“1”状态TAtom_{0 _0}在图6实际上代表了两个节点的iUML-B状态机。同样,在TAtom冲圆角矩形_{0 _3}在图7实际上代表了一个超级大国的iUML-B状态机,它包含两个亚态D1和D2。在Nth M层模型_N,功能状态机TAtom_{0 _0}首先是用来描述系统的事件序列,和事件b代码是自动生成的。此时,功能状态机模型没有时间约束和时间相关的不变量。这是一个完全“不计时的状态机,和M_N没有时间的约束模型。在N+ 1-th层,时钟状态机_{0 _1}是补充道。此状态机将执行一个事件周期性永远在初始化之后,也就是说,tick_tock事件。时钟tick_tock事件的影响是最小时间单位添加到值的全局时钟变量和本地时钟变量。生成的代码_{0 _1}底部是斜体标记的米吗_{N+ 1}层模型。为了把功能状态机状态机,第n个功能状态机TAtom_{0 _0}是提炼成N+ 1层TAtom_{0 _1}。精制方法如下:首先,一个本地时钟变量(例如:现在)补充道,和一个时钟复位动作(如:= 0)被添加到状态机的输入边缘节点需要添加时间限制;其次,一个不变的添加到节点(如状态节点一个= 1),需要添加一个时间约束;例如,

发票:现在≤T

在哪里T是一个常数的自然数类型。

这时,一个保安被添加在过渡边缘时间限制需要添加;例如,

后卫:现在>T

最后,一个动作被添加到tick_tock事件:

行动:现在:∣(一个= 1⇒现在' = + 1)

这可以确保只有当吗一个处于的状态一个= 1,时钟变量的值(也必须)会增加最小时间单位。

接下来,我们可以使用功能状态机和股票状态机逐步建立一个事件b模型的实时系统,它用作一次细化框架如图7。

在这种时间优化框架,系统模型从最初的抽象模型M0开始。M0层最简单的功能状态机TAtom_{0 _0}和股票状态机_{0 _0}。在M1层,我们添加一个新的状态或过渡(增量垂直细分)TAtom_{0 _0},这使得TAtom_{0 _1}。当然,我们也可以添加一个新的时钟变量股票状态机_{0 _0}使它成为TAtom_{0 _1}。在M2层,我们继续执行增量TAtom垂直细分_{0 _1}并添加一个新的功能状态机TAtom_{1 _2};然后,我们添加TAtom之间的约束关系_{0 _2}和TAtom_{1 _2}执行水平扩张。通过不断的使用这种方法,我们不仅可以提炼一个实时对象模型也不断向系统添加新的实时对象模型,直到最终实时系统模型。

本节的其余部分展示了如何实现各种细分模式在表1使用iUML-B状态机。由于空间限制,我们只使用三个例子来说明施工方法和过程。

4.2。逐步求精

4.2.1。准备一般施工方法

我们使用期限时间自动机的施工过程模式来说明逐步求精的原则,如图8。最后期限的原则模式来约束所有事件在一个状态机完成一定的期限。因此,我们遵循以下步骤完成细化的过程:(1)在不计时的细化,N层功能状态机TAtom_{0 _1}是提炼成N+功能状态机TAtom 1-th层_{0 _2}。添加一个新节点的N+ 1-th层和标记为状态2。新添加的节点然后变成一个新的初始状态节点,和一个新的事件e₃添加新节点与原相连TAtom初始状态吗_{0 _1}(一个= 0)。(2)一个新的时钟变量x和一个新的时钟常数T₁被添加在TAtom吗_{0 _2}机器。(3)TAtom上执行以下操作_{0 _2}:(我)一个动作被添加到事件e₃:行为:x:= 0(2)添加一个不变的原始状态机的所有节点,需要添加的最后期限约束:发票:x≤T₁(4)一个新的股票的操作添加到tick_tock事件_{0 _2},时钟的状态机N+ 1层:行为₃:x:∣(一个= 0⇒=x+ 1)行为₄:x:∣(一个= 1⇒=x+ 1)

上述步骤后,最后期限的要求模式可以实现;也就是说,TAtom的行为_{0 _1}有限状态机是完成T₁时间单位。

4.2.2。使用iUML-B状态机进行逐步求精

我们使用iUML-B状态机来执行各种增量改进指导下的通用方法。在这里只截止日期模式给出的一个例子。在图9剩下的这篇文章中,我们使用的超级大国iUML-B状态机来表示原子时间细化之前状态机。例如,在图9,B1是用来表示原子时间细化之前状态机。如果一个模式包含两个iUML-B时间状态机,我们将使用B1和B2代表他们,分别。

根据截止日期的定义模式如图1和定义3.2中,状态节点B1和初始状态B0构造模拟l₀节点和l₁节点图1后,系统将进入B0状态初始化。自从B0(即l₀)是在紧急状态下,有条件的约束添加到股票状态机的时钟x不会开始,直到它进入B1状态。此外,不变的x≤t添加到状态B1限制内完成吗t时间单位。这也意味着所有转换B1内必须完成t时间单位。当钟x到达t,时间将会“停止”,tick_tock事件将被禁用。

4.3。分解细化

需要强调的是,根据定义在UML中,状态分解和组合可以执行基于UML状态机图本身,但是,当我们说节3.1。2状态机的改进iUML-B非正式不如UML状态机的改进。简而言之,首先,iUML-B状态机的前端事件b。因此,它的分解和细化是基于事件b .其次的分解和细化,细化的iUML-B状态机必须遵循更多的规则,确保改进是正确的。第三,与国家iUML-B细化,细化的UML没有任何正式的语义的保证。关于两种建模语言的区别,说在她的博士论文中对此进行了详细讨论。

4.3.1。一般施工方法

时间间隔的原则分解细化分解是一个抽象模型为多个时间间隔的时间间隔,将按顺序执行(或选择、周期)的改进模型。这些间隔命名的子区间,子区间的速记。我们使用顺序分解澄清时间间隔的原则分解细化,如图10。

第n层模型图10是提炼成N+ 1-th层模型。它的主要作用是分解时间控制节点一个= 1在n层模型分为三个小区间N+ 1-th层模型,即SubInter1 SubInter2, SubInter3。详细的细化过程如下。(1)在不计时的精致,功能状态机TAtom n层_{0 _1}是提炼成N+功能状态机TAtom 1-th层_{0 _2}。状态机TAtom节点1_{0 _1}分解为三个节点TAtom吗_{0 _2},这是标记为1,2,3。事件e₃和e₄被添加到连接这些节点。(2)时钟变量x₁,x₂,x₃以及时间常数t₁,t₂,t₃被添加到N+ 1层模型。(3)TAtom上执行以下操作_{0 _2}:(我)行动”的行为:x₁:= 0”添加过渡边缘的事件e₁,不变的x₁≤t₁添加上e₁的目标节点(节点1);(2)保护接地的:x₁>t₁和一个行动”的行为:x₂:= 0”添加过渡边缘的事件e₃,不变的x₂≤t₂添加上e₃的目标节点(节点2);(3)保护接地的:x₂>t₂和一个行动”的行为:x₃:= 0”添加过渡边缘的事件e₄,不变的x₃≤t₃添加上e₄的目标节点(节点3);(iv)保护接地的:x₃>t₃添加到事件的转变e₂。(4)股票行情自动收录器状态机_{0 _1}是提炼成股票_{0 _2}。详细的改进过程,为每个节点具有时钟约束如果当前系统状态保持在节点,时钟变量对应节点增加了最小时间单位。例如,对于节点一个= 1,只需添加行动:一个= 1⇒=x₁+ 1)。(5)全球不变量补充道:发票:t₁+t₂+t₃≤T。

在上述过程中,步骤(1)是不计时的细化,不涉及任何时间信息;其他步骤细化。这些细化的步骤都可以在iUML-B状态机完成,和事件b代码如图10是自动生成的。代码与时间相关的控制流在斜体标记。

4.3.2。执行分解细化使用iUML-B状态机

我们使用序列优化模式来说明如何使用iUML-B状态机来执行分解细化。在序列优化模式中,一部分是分解的状态。原始的状态l分解为三个亚态l₃,l₄,l₅。添加新的州相连的事件一个₂和一个₃。另一部分是时间的分解。每个亚态都有自己的本地时钟。状态转换的先决条件是满足的约束的局部不变状态,如图11。

上的不变的l₃状态意味着,当系统处于这种状态,时间的价值x₃不大于t₃,所以下面的代码添加到tick_tock事件在股票状态机:

警卫:l_statemachine =l₃⇒x₃+ 1≤t

相似不变量添加到l₄和l₅州。应该注意的是,自从三个亚态分解从原始状态,最长时间的消费不能超过指定的时间上限由原状态。换句话说,全球不变量必须添加以下:

不变:t3 +t4 +t≤5t

4.4。横向扩张的

4.1.1。一般施工方法

在侗族的工作,水平扩张模式主要是用来描述两个实时对象之间的关系。精制框架在本章提出打算逐步添加新的并发对象而强加限制新的现有对象和对象之间的关系。我们模型共有6水平扩张模式使用iUML-B状态机。在本节中,只有施工过程的事件中断模式提出澄清横向扩张的原则,如图12。

事件中断模式的原理是,当外部事件发生时,无论哪个州一个状态机,它必须立即切换到另一个状态机的初始状态,并开始执行。前提是,已经有一个状态机的时钟变量x₁。由此产生的模型,这种扩张是一个新的模型合成系统的两个状态机。因此,我们执行以下精制过程:(1)一个新的状态机TAtom_{1 _2}添加在N+ 1-th层,其状态变量名与TAtom不同_{0 _1}。例如,如果TAtom的状态变量的名字_{0 _1}是一个,TAtom的状态变量的名字吗_{1 _2}一定不是,它被标记为b在图12。(2)在N+ 1-th层,TAtom_{0 _2}TAtom继承所有的州_{0 _1},过渡优势明显e₅从所有TAtom_{0 _2}对TAtom_{1 _2}是补充道。应该注意的是,这一步只需要添加一个过渡TAtom极权主义国家的边缘_{0 _2}TAtom的初始状态_{0 _1}罗丹的工具。(3)一个新的时钟变量x₂和一个新的时钟常数T₂是补充道。(4)一个新行为添加到tick_tock时钟状态机(股票的事件_{0 _2})的N+ 1层:行为₂:x₂:∣(b= 1⇒=x₂+ 1)

10/24/11。使用iUML-B状态机进行横向扩张

我们使用iUML-B状态机来执行事件中断水平扩张,如图13。

5。案例研究

在本节中,我们利用这段时间细化框架提出了构建事件b模式的一个典型的实时system-pacemaker控制系统。

5.1。起搏器的原则体系

心脏起搏器是一种医疗设备,调节心率。它可以感觉到心脏的活动和使用电脉冲控制心肌,使心脏跳动在规定的心率。心脏起搏器通常使用一种双线式装置和控制右心房和右心室的心肌,如图14。

起搏器的核心理念是如图15。如果心房或心室的收缩活动并不感觉到在指定的时间内,就会发出一个电脉冲刺激心房或心室的心肌,这样他们就可以在指定的心率。例如,在心房行图15,起搏器没有到达下一个同样的事件在指定的时间间隔内第一个心房击败事件后,它发出节奏信号(速度)。

摘要感应心脏活动的活动统称为感应心脏事件和节奏动作统称为节奏的事件,如心室感知事件或心房踱步事件。心房感知和心房节奏活动统称为心房事件,和心室的定义事件是相似的。在的功能模型图15,整个时间轴是由一系列的心脏周期。心动周期是解释为连续两个心室事件之间的时间间隔。一个₁∼一个_n指定一些心房事件的发生时间间隔后,和V₁∼V_k是时间间隔后心室事件的发生。当系统在一定的时间间隔,我们说这个区间是“活跃。”例如,在心房感知事件图15,一个₁∼一个_n是活跃的,在第一次心室感知活动,一个₁∼一个_n变得不活跃,V₁∼V_k变得活跃。表2给出了专业领域的术语起搏器。不同时间间隔的含义如下:(我)LRI:之间的时间间隔最长允许连续两个心室活动。如果没有心室活动发生在这个时间间隔内,心室起搏器必须出具事件(VP) LRI年底。心室感知事件(VS)可以阻止和重置LRI间隔。室后,传感事件(VS)或心室刺激事件(VP)发生,LRI间隔将重启。(2)URI URI:间隔由任何触发心室活动(VS或副总裁)。URI是活跃的时,起搏器不能发出心室刺激事件;也就是说,它不能触发副总裁事件。(3)AVI:它的目的是保持心房心室同步。之间的时间间隔是AVI连续心房和心室的事件。心房活动引发的AVI间隔(或AP)。如果没有感觉到在心室活动AVI间隔,心室刺激事件间隔结束后发布。AVI活跃时,时间间隔不会重置任何心房活动(或AP)和只能打断了心室活动(VS或副总裁)。应该注意的是,AVI间隔的持续时间比LRI间隔更短。(iv)VRP:它被定义为间隔室通道的输入信号不敏感。引发的VRP间隔VS或副总裁,可以通过内部心房停止活动。此外,VRP间隔小于LRI间隔。(v)PVARP: PVARP间隔是防止心房通道传感心室刺激事件由于串扰;因此不允许启动一个新的AVI PVARP期间间隔。PAVRP任何触发心室活动(VS或副总裁),可以在任何时候停止由心室感知活动(VS)。同样,PVARP间隔的持续时间比LRI间隔更短。为了防止心室活动的相声,PVARP间隔的持续时间必须超过VRP间隔。(vi)VABP:为了防止心室活动造成不必要的相声行为在心房频道和筛选潜在的噪音,有一个消隐期后(VABP)每个心室事件(副总裁VS)。VABP间隔期间,心房事件将被忽略。VABP触发心室活动与PVARP (VP)和重叠,所以VABP的时间必须比PVARP的持续时间短。(七)VAI:它也被称为心房逃脱间隔。这个区间代表最大可能延迟的发生心房心室后活动活动。VAI由任意触发心室活动。如果VAI间隔结束时,起搏器必须提供一个心房踱步事件;也就是说,AP事件必须被触发。如果检测到心房活动而VAI间隔是活跃的,VAI区间将被打断。VAI间隔的持续时间和AVI的持续时间等于LRI间隔的持续时间。VAI间隔和AVI间隔不重叠。

事件和各种时间间隔之间的关系表2如图16。事件和时间间隔排列的顺序从左到右的发生。作为事件发起一个新的AVI间隔和随后的副总裁事件终止它,开始一个新的心动周期。同时激活的时间间隔由副总裁事件在心动周期PVARP, VRP, LRI, URI和瓦。在第一个心动周期,由于VAI的最后,起搏器发出AP事件;因此,AVI间隔开始。之后,虽然AVI区间仍在活跃阶段,AVI终止和系统进入第二个心动周期,因为起搏器感知心室事件与心动周期,尽管LRI和URI都活跃,心房感知事件打断了他们的谈话,系统再次进入AVI间隔。因为这AVI间隔开始前,LRI AVI结束时仍活跃,但是,根据要求,必须有一个副总裁AVI结束后心室刺激事件问题。因此,LRI间隔终止和系统进入下一个心动周期。在第三个心动周期引发的新的副总裁事件,AVI间隔到来之前,它的结束时间是更早比URI。 But because the URI is the minimum constraint value for a cardiac cycle, the system must wait for the ends of the URI interval before sending a VP event.

心脏起搏器的原则是非常复杂的,在文献[详细解释31日]。我们不会在这里重复但只给每个事件的建模需求和时间区间如表所示3。

5.2。起搏器建模基于iUML-B时间状态机

我们使用iUML-B起搏器的状态机建立事件b模型框架的指导下提出了部分4。我们的基本想法是模型所有时间间隔状态的节点iUML-B状态机。每个区间都有自己的时钟变量、常数,和不变量。时钟变量区间的重置当系统进入这个区间。在一个区间,时间可以流逝只有在时钟变量是在允许的范围内的时钟不变量区间。当时钟变量的值超过的边界时钟不变,树叶状态触发一个事件。根据时间间隔之间的关系,我们首先模型最长的时间间隔,即LRI和URI作为最顶部的时间间隔,其中包括其他所有的间隔。然后,按顺序发生的时间间隔被建模为一个连续的分解模式的抽象模型,并在同一时间发生的时间间隔被建模为一个平行的组合模式。

为了表明我们的方法可以方便建模,将事件b模型的时间自动机模型,给出了映射规则从iUML-B UTA状态机:(我)“初始化”的状态节点指出过渡的边缘iUML-B状态机是映射到UTA的初始状态节点。(2)iUML-B状态机的状态没有时间限制节点映射到“承诺”或“紧急”UTA的节点。(3)iUML-B状态机的状态标注时间约束(即。,一个n我nterval) are mapped to the nodes of UTA marked with the same time constraint, that is, those nodes that are neither “Committed” nor “Urgent;” the invariants of these states can be directly mapped to the invariant of the corresponding node of UTA.(iv)“保护”和“行动”过渡的边缘iUML-B状态机映射到相应的位置的“保护”与“更新”的一部分UPPAAL时间自动机,分别。(v)iUML-B伪状态节点的状态机(如分支和聚合节点)可以被映射到UPPAAL的伪状态节点时间自动机或“承诺”或“紧急”UTA的位置。

我们使用这些规则翻译事件b模型相应的UTA模型的每一层。时间自动机模型添加到系统整体模型中一步一步根据事件b模型的逐步求精的过程。

5.2.1。抽象模型(0层模型)

LRI和URI间隔代表两个心室之间允许的最大时间间隔至少事件和最小时间间隔的流逝,分别。通过对图的分析16,它可以发现LRI和URI通常由同一事件引起的。至于响应事件副总裁完成后这两个时间间隔,以下事实也是如此:首先,副总裁必须发生后的URI;其次,如果URI已经结束但LRI尚未结束,会有两种情况:一种是LRI触发VP事件的结束,第二是AVI LRI之前结束结束;那副总裁事件引发的AVI的结束。在这两种情况下,URI和LRI的时钟变量将被重置为零。此外,在接下来的副总裁或对事件到来之前,即使URI已经结束,它不能被重置。因此,LRI和URI被建模为相同的时间间隔,如图(17日)。我们提出相应的UPPAAL时间自动机模型图17 (b)。应该注意的是,在图17和保持数据在本节中,之间没有完整的语义等价iUML-B状态机和相应的UPPAAL时间自动机。这个等价需要证明在后续工作。

有三个URI_LRI间隔触发事件:VS,副总裁,初始化。初始化意味着时间间隔被激活后,模型初始化。在任何时候,可以中止URI_LRI间隔和因此,根据时间事件前缀模式,我们构造一个“任何”状态,让它连接到URI_LRI状态通过VS事件。然后,我们重置时钟URI_LRI_clock的行动和事件。此外,事件副总裁之后才可能发生的时间间隔URI_LRI_DLY_DUR已经结束,必须发生在年底前URI_LRI_DDL_DUR。根据相关的延迟模式的定义,我们添加一个卫兵VP事件:

警卫:URI_LRI_clock≥URI_LRI_DLY_DUR

然后,我们添加一个警卫tick_tock事件的股票状态机根据截止日期的定义模式:

警卫:URI_LRI_clock + 1≤URI_LRI_DDL_DUR

这将停止时钟,当它到达URI_LRI_DDL_DUR。

5.2.2。第一层优化模型

在这种水平的优化,我们将URI_LRI区间划分为两个小区间,即ventricular-atrial间隔(VAI)和实力东移区间代表的时间间隔在收到一个心房的事件。我们有AVI≤实力东移和VAI +实力东移≤URI_LRI。这两个间隔时间顺序发生。因此,我们使用顺序分解模式子区间模型作为独立的州VAI和实力东移,如图(18日)。事件和美联社代表心房感知事件和心房踱步事件,分别。我们添加一个UPPAAL时间自动机模型“瓦”图18 (b),时钟“t”VAI的本地时钟时间自动机和常数“TVAI”对应于VAI_DDL_DUR常数在图(18日)。除非另有规定,本节剩下的图将遵循这一重命名规则。如果“| |”代表了时间自动机的成分,那么当前全球时间自动机模型(命名系统)可以表示为

系统URI = | | VAI

遵循VAI的实力东移间隔间隔和AP或引发的事件。作为事件位于VAI间隔和结束的开始感觉间隔和VAI_DDL_DUR内可能发生的时间。美联社,VAI的反应的结束和实力东移的触发,VAI_DDL_DUR之前VAI_DLY_DUR后必须发生。根据这些需求,我们重置实力东移的本地时钟ASensed_clock,美联社事件发生时。此外,我们添加一个警卫根据截止日期的定义随着事件的模式:

警卫:VAI_clock + 1≤VAI_DDL_DUR

并添加警卫美联社事件根据延迟模式的定义和期限模式:

Guard1: VAI_clock + 1≥VAI_DLY_DUR

Guard2: VAI_clock + 1≤VAI_DDL_DUR

5.2.3。二级优化模型

在这种水平的优化,我们继续完善实力东移间隔。根据原理图16节5.1,心房事件和美联社将触发AVI间隔。因此,在这种程度的改进,我们将为AVI间隔和美联社的事件。此外,结束的AVI间隔可分为三种情况:第一种情形是AVI VS中断事件,系统进入VAI间隔;第二个情况是URI已经成为活动结束后的AVI间隔;然后需要触发事件执行副总裁心室步伐;在第三情况,URI AVI间隔结束后仍然活跃,所以起搏器需要等待结束的URI进入下一个心动周期。我们使用XOR模式和序列模式模型这三种情况下,如图(19日)我们添加一个UPPAAL时间自动机模型“AVI”图19 (b),时钟“时钟”是这个时间自动机的本地时钟和时钟“t”是全球整个系统的时钟。现在,当前全球时间自动机模型可以表示为

系统URI = | | VAI | | AVI

5.2.4。第三个层次细化模型

在第三层次的细化,我们进一步完善VAI间隔。首先,根据部分中描述的原则5.1VRP间隔和PVARP区间重叠的时间表,和他们的关系符合并行组合模式。因此,我们分解VAI间隔成并行蚁群的组成和PVARP。其次,根据江泽民的工作(32之前),我们把VABP PVARP(这将使我们在图模型和时间表16不一致的。尽管这可能看起来很奇怪,我们认为江泽民的分析更专业),如图20(一个)。我们添加两个UPPAAL时间自动机模型“VABP”和“与”图20 (b)和图20 (c)。现在,当前全球时间自动机模型可以表示为

系统URI = | | VAI | | AVI | | VABP | | VRP

我们可以继续使用横向扩张模式和垂直细分模式提出了得到一个更复杂的iUML-B起搏器的状态机模型。本节中的案例研究只是证明我们提出的建模框架的实用性和iUML-B时间状态机模式。此外,我们表明,iUML-B时间状态机可以很容易地转换成UPPAAL时间自动机。这是因为我们使用iUML-B状态机模仿UPPAAL从开始时间自动机。

6。讨论

在本节中,我们比较了现有的实时事件b方法的方法。我们给六个评估标准,如表所示4。

“时间限制”模式的原理图所示(21日)。事件命名tick_tock用于进展时间,也就是说,增加时钟变量的值。事件命名post_time是用于添加一个或多个时间限制,和一个事件命名process_time用于删除一个或多个时间限制。的限制下“时间限制”模式,如果增加时钟变量的最小时间约束(例如,at1图(21日)),process_time事件没有删除这个约束,系统将“停止”,这是“约束”是什么意思。时间限制模式只是一种设计方法。它没有提供一个机制来表达事件的顺序以及时间。换句话说,人们只能手动添加事件b代码为了控制事件的顺序和描述时间。它不能表达并发实时对象,所以很多手工编码建模时需要一个稍微复杂的实时系统。此外,它不提供任何插件自动生成的证明义务,也不支持改进(包括横向扩张和纵向细化)过程的实时系统。

“过程模式”的原则如图21 (b)。它使用一个事件bt(这意味着“真正开始”)来改变一个谓词P从假到真同时重置计时器的值D为0。一个事件命名抽搐会增加的价值D只有当P是真的。时的值D达到一定常数c会触发另一个事件。除了一个变量D是用来表达时间,“时间模式”的缺点是一样的时间限制模式。

“时间属性”方法是成熟和完整的实时事件b建模方法。它使用三种模式命名的最后期限(一个;B;t),延迟(;B;t),到期(一个;B;t)代表期限、延迟和超时场景实时系统和为这些时间模式提供了严格的语义事件b。时间属性方法使用一个树状图人队(事件精制结构图33])来表达事件的顺序和精致的结构,从而支持实时事件b模型的细化和分解。此外,Sarshogh还复合材料三种模式形成各种复杂的实时事件b精制模式。时间属性方法的原理图所示22。建模者可以使用时机插件来添加时间限制,自动生成证据的义务,并自动排放这些证据的义务。Sarshogh声称大部分的证明义务(95%)可以与自动出院定理验证。因此,时间属性方法可以支持事件b建模的大型和复杂的实时系统以及自动一致性的证明。但时间属性方法不支持并发实时对象的表达式。虽然人图可以表达垂直事件分解关系,它不够直观表达事件的顺序在一个特定的优化水平。人们需要通过分析理解事件的实际订单。

提出的时间间隔方法Sulskus使用“时间间隔符号”来表达不同的时间限制。它添加了一个更高级的区间的概念,扩展了时间符号,并介绍了中止活动。此外,时间间隔方法使用一种改进的人图让事件分解关系的表达式在垂直细分流程清晰。例如,广场上标有“Sub-Int”是用来表达子区间,和一个正方形标有字母“P”是用来表达并行成分个子区间的关系。时间间隔方法也使用iUML-B状态机来表达事件在一个特定的顺序优化水平以及并行实时并发对象的组合。时间间隔的方法的一个例子是图所示23。Sulskus也提出了各种成分的实时事件b细化模式,并使用“tiGen”插件来表达时间间隔以及自动生成证明义务确保改进一致性。事件b模型中的三个复杂实时系统由使用时间间隔方法,100%的自动证明证明义务。

可以看出,使用各种自动化的方法插件来支持事件b中的实时系统建模框架越来越强大。但这些方法可以避免事件b本身的缺点;,他们也不会支持各种时间属性的表达式和验证(如需要公平和活性等性质和类似TCTL属性),也不能“自然”保留这些属性在细化过程。黄平君和施耐德说,[34”,挑战在于如何识别更自然的方式整合事件b和LTL LTL属性可以通过事件b保存细化,这并非如此。“我们的观点是,最好和比集成更容易采用集成的正式方法事件b和LTL属性验证使用的语法和语义事件b就像Iliasov和虚荣所做的工作等。

本文中的方法使用iUML-B功能状态机来表达事件的顺序在一个特定的细分水平和使用股票状态机来表达时间的推移。我们使用iUML-B状态机的状态节点来表达时间间隔Sulskus一样,除了我们的方法需要手动添加各种时间不变量状态节点,而不变量的时间间隔自动生成方法。表达事件分解的垂直细分的水平之间的关系,我们的方法比约束方法和持续时间的模式,但它不是清楚的人图时间属性方法和时间间隔的方法。你必须观察和比较两种细化级别的状态机来了解N事件被分解成水平N+ 1-th级别的事件。在并发实时对象的表达方面,我们的方法是最优的。我们借用盾的时间自动机的概念模式,提出各种横向扩张模式,更有利于事件b模型的复杂系统建模与大量的并发实时对象。

我们的方法的限制是,我们不提供任何插件支持自动生成和自动定理证明的证明义务。这是因为我们工作的动机是消除之间的语法和语义差距基于事件的正式系统和automata-based正式系统,以便事件b模型可以更容易地转换为一个时间自动机模型。因此,时间事件b模型可以容易验证的属性。

与现有的各种方法,直接将事件b模型UPPAAL时间自动机,我们只希望把“时间方面”事件b模型的时间自动机。原因在于,首先,有许多unmappable部分语法元素之间的事件b模型和UPPAAL的时间自动机。例如,大量的离散数学表达式的事件b模型不能直接转化成UPPAAL模型。第二,当事件b模型非常复杂,这个翻译过程非常耗时的,特别是当这些事件b码产生的自动代码生成工具(比如tiGen)。

评估各种实时事件b建模方法包括我们的方法在表5。

7所示。结论

定理证明语言通常使用一阶谓词逻辑作为其理论基础,所以它有很大的局限性在表达时间和验证时间属性。但是,对于软件工程师,一个正式的系统事件b非常适合基于定理证明系统抽象模型来具体模型的开发过程以及软件代码。因此,使用事件b来建模实时系统是一个不可避免的方法来验证复杂的软件。当前实时事件b建模工作主要侧重于事件b中的建模和定理证明方法框架,带来更多的学习成本和理解的障碍。提出了一种实时系统建模和优化框架基于iUML-B状态机,在这一系列的可重用的事件b设计模式建模实时系统。使用这些模式,建模者可以迅速建立一个实时系统的事件b模型并将其转换为一个时间自动机模型完成时间属性验证。

在未来,我们将继续研究自动翻译方法从iUML-B时间状态机UPPAAL时间自动机和证明翻译过程的正确性。

数据可用性

数据支持这一研究可以从相应的作者。

的利益冲突

作者宣称没有利益冲突。

确认

这项研究得到了陕西省自然科学基金项目、中国(批准号2020 jm - 633)和项目的陕西省的关键研究和发展项目,中国(批准号2020 gy - 084)。