信息物理融合系统(CPS)[1]是计算过程和物理过程的融合系统.它强调信息世界与物理世界的融合,强调对交互环境的实时监测与控制.它通过与交互环境的实时交互来增加或扩展新的功能,以安全、可靠和实时的方式检测或者控制一个物理实体[2].实际上,CPS核心是3C(computation,communication,control)融合,自主适应交互环境的变化.从其交互环境的角度来看,其功能的关键是感知与控制.而感知与控制对时间非常敏感,因此,时间需求在CPS中非常重要.由此,我们提出对CPS的时间需求进行建模与验证.
需求存在于环境之中[3],CPS的时间需求也来自于其交互环境.所谓交互环境,指的是所有将要与CPS软件交互的实体.由于CPS软件应用的广泛性,其交互环境实体多样,可以是自然环境、建筑、机器、物理设备等等,当然也包括人类自身.这样的环境可以被实时感知,部分(如物理实体)还可以被控制.这些异构的环境实体导致交互出现多样性,使得时间度量本身可能存在多种形态(比如用距离、角度来衡量时间).而且由于交互是实时交互,正是通过交互才实现了CPS的功能,因此,CPS的时间需求的建模有3个要求:1) 必须建立在功能性需求之上,与功能性需求无缝地联系在一起;2) 在需求模型中,时间必须被显式地建模,与功能性需求的基本概念类似,时间必须作为第一类概念存在;3) 时间应该存在多种形态,且能够被定性与定量地描述.另外,由于CPS功能表现为其对交互环境的感知与控制,因此在需求模型的选择中,其功能性需求必须与物理实体的变化有关.
目前,代表性的需求建模方法有基于目标的方法[4]、基于主体与意图的方法[5, 6]和基于问题框架的方法[3, 7].面向目标的方法以目标为需求来源和依据,在时间需求建模上,它使用带类型的一阶时序逻辑作为语言,包含传统的时序算子和描述涉及实时节点特性的附加实时算子.面向主体和意图的方法提供一种基于组织层次上下文的需求获取和建模的思路,其建模理念为刻画有目的的参与者.它们也采用带类型的一阶时序逻辑语言来描述时间需求.这些时间需求工作都基于时序逻辑,可以描述定性约束.为了描述定量约束,人们进行了各种扩充,如Timed Computation Tree Logic[8]等.它们通常用于表示实时系统的性质和规范,在需求工程中用到较多的是一阶时序逻辑和谓词时序逻辑.由于目标和有目的的参与者等与物理实体、交互之间都不存在直接关系,因此,基于目标的方法和基于主体与意图的方法都不适合建模CPS.
与上述需求建模方法不同,问题框架方法认为,软件系统对现实世界的作用是软件问题的来源,对软件系统将与现实世界(交互环境)发生的作用进行结构化分析是需求分析的切入点.问题框架方法强调需要对软件系统将要作用的现实世界进行刻画,并将需求的含义指称到对现实世界相关领域的描述上.其建模的基本概念是现实世界中的问题领域(环境实体)以及未来软件系统与领域的交互.
我们认为,基于问题框架的方法适合对CPS进行功能需求建模,因为问题框架的方法可以用交互与其引起的物理环境变化描述功能.基于问题框架的方法,我们曾结合MARTE(modeling and analysis of real-time and embedded systems)[11]及CCSL(clock constraint specification language)[12]做过一些时间需求建模工作[9, 10].基于这些工作,本文将逻辑时钟引入问题框架方法,提出构建CPS时间需求一致性分析框架.
逻辑时钟特别适合建模CPS时间,它有如下好处:1) 逻辑时钟是一个抽象概念,可以表述和测量事件的有序多次发生.一个事件可以对应为一个逻辑时钟,事件的每次发生看作该时钟的一个时间点(或者说该时钟tick了1下).2) 逻辑时钟建模中重要的是时间点之间的序关系.一个时钟相邻时间点之间的物理时间间隔可以不同.我们也可以约束某一时钟,使其每次tick之间间隔相同,在此意义上,物理时钟可以看作逻辑时钟的一个特例.3) 它不限于常用的物理时间(比如手表时间),还可以由用户来定义,关联到任何实体上(例如温度、距离、角度等),支持多形态时间.
从上述描述中我们可以看出,将逻辑时钟引入问题框架方法来建模CPS的时间需求非常合适:功能性需求的基本概念问题领域和交互都可以与时钟关联起来,不同的问题领域可以建立不同的逻辑时钟,其时间点就是交互的每次发生.这样,时间需求就与功能性需求无缝地联系在一起.因此,本文提出引入逻辑时钟到问题框架的方法中,为CPS时间需求进行建模,利用时钟之间的关系定义CPS的交互环境约束,由此提取出软件时间需求规约.由于我们以前的工作[10]重点介绍了多形态时间,因此这不是本文的侧重点.本文重点建模时间需求的定性与定量关系,其中,定性的关系包括“时间点a发生在时间点b之前”之类的描述,定量的关系包括“时间点a发生时间点b之前,并且之间间隔等于(大于、小于)某一时钟的t个时间单位”这样的描述.
为了获得一致的时间需求规约,我们首先给出了其时间需求的概念模型,给出了其形式化语义以精确描述时间需求,定义了一系列定性和定量的时钟关系.在此基础上,定义了问题领域级别上的时钟构造算子,由此来构造系统级别的时间需求规约.以形式化语义为基础,我们定义了一致性属性,并将其表达为时态逻辑CTL公式.由于其语义为由标号迁移系统给出的状态变迁模型,本文选择使用NuSMV——一个经典的模型检测工具,来验证时间需求规约的一致性.
本文第1节简单介绍背景知识,包括问题框架方法、问题图、MARTE/CCSL以及模型检测器NuSMV.第2节定义时间需求的概念模型.第3节定义其形式化模型.第4节给出时钟构造算子以构造更高级别的时钟.第5节验证时间需求规约的一致性.第6节给出建模和验证过程,并用一个简单案例来展示方法的可行性.第7节比较相关工作,总结全文并提出进一步的工作.
问题框架方法是一个经典的需求工程方法[3, 7],用来建模、分析和结构化现实世界的需求问题.问题图是其功能性需求的描述模型,其基本元素如下:
机器,如图 1所示的Controller machine(缩写为CM),形状为一个带双竖线的矩形框,表示要开发的软件.
问题领域,如图 1所示的Device,形状为一个矩形框,表示机器将要交互的实体.
需求,如图 1所示的Work regime,形状为虚线椭圆框,表示文字描述的需求.
行为交互,如图 1所示的CM!{on,off},形状为为实线,表示机器与问题领域之间的交互,其中,CM!表示为CM发起,on,off表示现象.
期望交互,如图 1所示的{is_on,is_off},形状为虚线箭头,表示在问题领域上期望看到的现象.
![]() | Fig. 1A simple problem diagram图 1一个简单的问题图示例 |
MARTE是OMG组织认可的实时嵌入式系统建模语言[11, 12],CCSL是在其上开发的时钟约束语言.CCSL提供了一些元素来表达时间和时间约束,其时间的基本元素为时钟.时钟为一个五元组,如定义1所示.
定义1. 时钟(clock):
其中,I是时间点集;是I上的偏序关系,命名为严格先于;D是一组标签;λ:I→D是一个标签函数;u是一个符号,代表时间单位.时钟可以是物理时钟,也可使是逻辑时钟.物理时钟参考物理时间,逻辑时钟参考逻辑时间.一个逻辑时钟是由一组离散的有序时间点组成,这些时间点为事件出现的时刻.当时钟tick时,表示事件发生一次,可以用时序+1表示.因为它离散,可以通过自然数对I中的元素进行排序.对于任意的离散时钟Clock
<IC,pC,DC,lC,uC>,C[k]表示IC中的第k个时间点.下文中,在不会引起歧义的情况下,我们省略下标C.
两个时间点之间可以存在如下的时序关系:
同步
.它是一个很强的关系,强迫时间点发生的同步性.它具有对称性,也就是说,
,如果a≡b,那么b≡a.
严格先于(strict precedence,
).它表示时间点发生的严格时序关系.它有传递性,也就是说,∀a,b,c∈ Instant,如果a
b,b
c,那么a
c.
先于(precedence,
,等价于(
≡).它表示时间点发生的时序关系,具有传递性和自反性.
排除(exclusion,#
∪
).它表示这两个时间点永远不会在同一时刻发生.
NuSMV是一个经典的得到广泛应用的模型检测工具[13],可以验证有限状态系统是否满足用时态逻辑公式描述的性质.它支持多种建模方式,包括有限状态自动机(FSM).
FSM方式建模系统的基本概念有:一个系统包括多个模块(module),每个模块由模块名和模块定义组成,模块定义由形参(parameter)和主体(body)部分构成.每个模块主体定义一个FSM,变量声明在(VAR)部分,用来建模FSM中的状态,初始化约束(INIT constraint)决定FSM的初始状态,迁移约束(TRANS constraint)用命题公式描述FSM中状态迁移关系(状态变量的当前值及下一个状态的值).一个系统中要有一个main模块,且main模块不能有形参.通常,在main模块中实例化并调用需要的模块,这些模块实例描述的FSM的同步乘积(synchronous product)构成该系统的FSM.
下面是NuSMV FSM模型的一个小例子,它包括两个MODULE:
一个是main模块声明两个布尔变量,初始化为假,并创造了另一个模块subClock的一个实例;
模块subClock有两个参数,它的迁移约束限制每个状态下这两个参数的赋值只有3种情况:1) 都为真;2) 左边参数为假,右边为真;3) 都为假.
MODULE main
VAR
c1: boolean;
c2: boolean;
ctr1: subClock(c1,c2);
INIT
c1=FALSE & c2=FALSE;
MODULE subClock(left,right)
TRANS
(next(left)=TRUE & next(right)=TRUE)|(next(left)=FALSE & next(right)=TRUE)
|(next(left)=FALSE & next(right)=FALSE);
我们以前的工作[14]构建了一个功能性需求的概念模型.由于该功能性需求基于交互环境的变化,它适用于CPS系统.本文将这个模型进行扩展,加入与功能相关的时间概念,由此得到一个时间需求概念模型,如图 2所示.
![]() | Fig. 2Timing requirement conceptual model图 2时间需求概念模型 |
在图 2中,
白色的矩形框及其关联表示了功能需求的基本概念及其关联,它表示了基于交互环境变化功能性需求的基本概念:一个问题(problem)位于一组现实世界的问题领域(problem domain)中,其目的就是要开发一个机器(machine)来满足需求(requirement).其中,问题就是要由软件开发完成的任务,需求是需要完成的功能,机器则是要开发的软件,问题领域就是将要与机器交互的现实世界实体.一个问题领域可以是基本领域(basic domain),也可以是组合领域(combined domain).基本领域是一个现实世界实体,而组合领域则是可以由若干基本领域组合而成的领域.在机器与问题领域之间共享的现象,称为交互(interaction).
灰色矩形表示与时间相关的概念,包括时间点(instant)、时间点关系(instant relation)、时钟(clock)以及时钟关系(clock relation).时间点就是交互发生的时刻,它们之间的关系称为时间点关系.时钟是用来显示、协调时间的一个可视工具,系统时间可以看作一组时钟的集合.需要指出的是,时钟使用的是逻辑时钟,每个时钟拥有一组有序关系的时间点.为了可视地表示时间点及时间点的关系,我们定义时间点图(instant graph)为一个有向图,其结点是时间点,边为时间点关系.根据是否带有数量,时间点关系可以分为定性(qualitative relation)与定量关系(quantitative relation).定性关系主要是MARTE/CCSL中的4种关系,分别为coincidence,strict precedence, precedence和exclusion.这些关系描述了时间点发生的先后顺序关系.至于两个时间点之间的定量关系,该量化数值必须基于某一时钟的度量,这称为参考某个时钟.若两个或多个时钟的多个时间点之间存在关系,则时钟之间存在时钟关系.
上述两组概念通过如下的关联联系在一起:每个问题领域都拥有(或参考)某一个时钟,问题领域的每个交互发生的时刻都是该时钟对应的一个时间点.
本节拟给出时间需求概念模型中概念的语法与操作语义.由于概念时钟关系内容较多,所以分为基本概念与时钟关系两个小节进行描述.本文中的操作语义由标号迁移系统(labeled transition system,简称LTS)[15]给出. LTS是一种传统的广为接受的基于抽象状态机的状态变迁模型,一个LTS由一个四元组(S,s0,A,T)组成,分别代表系统状态集合、初始状态、动作标号和迁移关系.LTS可以直观地用图形表示,状态表示为圈,迁移表示为圈之间的有向箭头,标号标于对应箭头上.为了方便理解,时间点关系、时钟关系和下一节中的时钟构造算子的操作语义都用LTS图形式给出.
根据概念模型,问题领域可以由它的身份标识和问题描述定义,因此我们给出如下定义:
定义2. 问题领域(pd):
pd<id,pdescription>.
其中,id是问题领域的标识,pdescription是问题领域的描述.
交互是问题领域与机器之间共享的现象,因此交互可由发起方、接收方及共享内容定义:
定义3. 交互(interaction):
Interaction<idint,initiator,receiver,hasContent>.
其中,idint是交互的标识;initiator是现象的发起方,可以是问题领域(或机器);receiver是现象的接受方,可以是机器(或问题领域);hasContent是接受方和发起方共享的现象.
由于时钟与问题领域关联在一起,因此本文将时钟定义为d.C的形式,其中,d表示问题领域,C表示与它相关的时钟.由于本文重点不在多形态时钟,因此在定义1的基础上,将时钟定义简化为一个二元组:
定义4. 时钟(d.C):
d.C<I,
>.
其中,I是领域d的所有交互发生时刻的时间点集;是I上的偏序关系,也称为严格先于.我们定义函数idx:I→
用来取得时间点在时钟的时间点集合中的编号,对∀i∈I,idx(i)=k当且仅当i在I中的编号为k.
在此基础上,将整个时间系统定义为一组时钟的集合,标记为T={d1.C1,d2.C2,…,dn.Cn},其所有的时间点集合标记为TI.不同问题领域的时钟可能不具有可比性,它们有不同的tick速率和不同的形式.在一个系统当中,不一定有全局时钟.
不同交互发生的时间约束可以通过对应的时间点之间的关系来衡量,我们定义时间点关系.
定义5. 时间点关系(TR)包含两种关系:定性关系(IL)与定量(IT)关系.
IL:TIxTI
定性关系IL与MARTE中定义的4种关系相同,即,包括coincidence,strict precedence,precedence和exclusion.
定量关系IT由定量算子op给出.由于定量关系需要考虑量度问题,所以op与时钟密切相关,其定义 如下:
其中,idxC3(n)表示时钟C3的时间点n在IC3中的编号.该定量关系约束时钟C1的第i个时间点与时钟C2的第j个时间点之间的区段中时钟C3 tick等于(或大于、大于等于、小于、小于等于)k下,其LTS语义如图 3所示.在图 3中,Φ为一特殊标号,表示没有时钟tick,它包含3个状态:状态0、状态1和状态2.当约束处于状态0时,时间点C1[i]可以发生,它的发生使得算子进入状态1,当算子处于状态1时,时间点C2[j]才可以发生.这保证了时间点C1[i]先于C2[j]的时序关系.由于该算子只描述这两个时间点之间的关系,当两个时间点都发生后,该算子不再约束,状态2只有到自身的Φ变迁.
![]() | Fig. 3LTS semantics of instant relations图 3时间点关系的LTS语义 |
在CPS这样的复杂系统中,交互可能无数次发生,只定义其中一部分时间点关系远远不够.因此,我们尝试在问题领域级别的时钟上建立关系,即,在时钟层面定义关系来描述和反映时钟之间时间点的对应关系.
时钟之间的关系由时间点之间的关系来定义.时间点关系有定性与定量之分,因此,我们将时钟关系也分为定性关系与定量关系.定性关系可以包括很多,用户也可以自己定义,本文仅仅给出3种比较常用的关系: subClock,fasterThan和alternate.
定性关系1.d1.C1 subClock d2.C2是子时钟关系,它表示在一个时钟d1.C1的时间点发生的同时,其父时钟d2.C2一定有对应的时间点发生.两个时钟对应的问题领域应该也具有父子关系.该关系成立,如果
满足如下关系:
1) h是单射;
2) h单调:
3) 时钟d1.C1的每个时间点与其对应的d2.C2的时间点同时发生:
图 4给出了d1.C1 subClock d2.C2的LTS的语义,其只有1个状态,表示在任一时刻(同一条迁移上),要么两个时钟都tick,要么父时钟tick子时钟不tick,要么两个时钟都不tick.
![]() | Fig. 4LTS semantics of d1.C1 subClock d2.C2图 4d1.C1 subClock d2.C2的LTS语义 |
定性关系2.d1.C1 fasterThan d2.C2表示时钟d1.C1的第i个时间点要先于时钟d2.C2的第i个时间点发生.
它有两个版本:严格的strictPre和非严格的nstrictPre,该关系成立,如果满足如下条件:
1) h是单射;
2) h单调:
3) 时钟d2.C2的每个时间点与其对应的d1.C1的时间点有序:

d2.C2的每个时间点可以发生的条件是,该时间点对应的d1.C1的时间点已经发生过了.为了确保d2.C2不过早tick,我们需要监控d1.C1已经提前(相对于d2.C2)tick了多少下,所以在其LTS语义中(如图 5所示),我们记录两个时钟已发生过的时间点的个数的差值δ=idx(d1.C1)-idx(d2.C2),不同的状态对应于不同的δ数值.由于d1.C1比d2.C2快,δ≥0.算子所处的状态(即当时δ的值)决定下一个时刻哪个时钟可以tick.例如严格版本中,当δ=0时,只有d1.C1可以tick,那么当d1.C1 tick而d2.C2不tick时,差值δ加1,算子状态迁移到状态s1.以此类推,算子在状态s1(δ=1)表示d1.C1已经比d2.C2多tick了一下,那么接下去的时刻,可以d1.C1单独tick使得δ加1;或者d2.C2单独tick使得δ值减1;或者d1.C1和d2.C2都tick,那么δ值不变;或者两个时钟都不tick,当然δ值也不变.
![]() | Fig. 5LTS semantics of d1.C1 fasterThan d2.C2图 5d1.C1 fasterThan d2.C2的LTS语义 |
定性关系3.d1.C1 alternate d2.C2表示时钟d1.C1和d2.C2交替tick,从左边的时钟开始,该关系成立,如果
满足:
1) h是单射;
2) h单调:
3) 两时钟时间点交替发生:
其LTS语义如图 6所示.初始时只有d1.C1可以tick.它tick后,算子进入状态s1,d1.C1将不可以连续tick,只有d2.C2可以tick,使算子回到状态s0.如此往复.其运行序列将为d1.C1;d2.C2;d1.C1;d2.C2;…
![]() | Fig. 6LTS semantics of d1.C1 alternate d2.C2图 6d1.C1 alternate d2.C2的LTS语义 |
定量关系表示两个时钟的时间点之间存在某些量化关系.定量关系也很多,用户也可以自己定义.本文仅给出最常用的boundedDiff(i,j).
定量关系1.d1.C1 boundedDiff(i,j) d2.C2表示这两个时钟的时间点之间的时间差在整数闭区间[i,j]之内,i为负整数,j为正整数.可以把boundedDiff看作fasterThan的一个扩展,限定了差值δ的边界,但不规定哪个时钟更快,如图 7所示:当下届到达时,右边的时钟不能在下一个时刻单独tick;而当上界到达时,左边的时钟不能在下一时刻单独tick.
![]() | Fig. 7LTS semantics of d1.C1 boundedDiff(i,j)d2.C2图 7d1.C1boundedDiff(i,j)d2.C2的LTS语义 |
在已定义的时钟基础上,为了进一步构造问题领域级的时钟及系统级时钟,本节拟定义一些时钟构造算子.由于我们的模型的时钟与问题领域相关,时钟构造算子可以分为两类:一类针对单问题领域,另一类针对组合问题领域.
这种情况发生在一个问题领域的某些交互周期性发生的时候,这个领域(或者子领域)对应的新时钟就可以通过二进制字符(binary word)当前位(0或1)选择所有交互的一部分发生而构造(0表示舍弃,1表示保留),即,过滤出时钟的一部分时间点,这种算子称为filteredBy.
定义6. filteredBy:
d.Cd1.C1▲w.
根据已有时钟d1.C1和二进制字符ω创建新时钟d.C,该关系成立,如果满足如下条件:
1) h是单射;
2) h单调:;
3) 时钟d1.C1的任一时间点与其对应的d.C的时间点同时发生:
其中,ω↑k表示ω第k个“1”的位置,当时钟d1.C1 tick并且w的当前位(current bit)为“1”时,时钟d.C tick.通常,ω写作u(v)ω,u为初始部分,v为重复部分.这时,d.C被创建为d1.C1的周期性时钟,周期为v的位数.
例如,d.Cd1.C1▲0(01)ω的LTS语义如图 8所示:在d1.C1第1个时间点tick之后,算子进入状态s1,之后的运
![]() | Fig. 8d.C![]() ![]() |
行序列将为d1.C1;d.C,d1.C1;d1.C1;d.C,d1.C1;…图 9是其工作原理的直观展示.
![]() | Fig. 9Instant graph of d.C![]() ![]() |
在已知两个或多个子领域的时钟情况下,如何获得组合领域的时钟,与领域的组合相关.根据领域结构的不同,问题领域的组合可以分为两种类型:一种为相同结构领域组合,另一种为不同结构领域组合.所谓相同结构领域,指的是这些领域与机器之间共享相同的现象.
首先,若两个问题领域结构完全不同,则二者的组合对应的时钟时间点集应该是二者的时间点集的并,称为union,其具体定义见定义7.
定义7. union:
d.Cd1.C1 union d2.C2.
根据已有时钟d1.C1和d2.C2创建时钟d.C.d1,d2为时钟C1,C2所属不同的问题领域,d为它们的并.每次d1.C1或d2.C2tick,时钟d.C同时tick,时钟d.C与时钟d1.C1和d2.C2的关系满足:
d1.C1 subClock d.C;
d2.C2 subClock d.C;
直观上理解,时钟d1.C1(d2.C2)的任一时间点与d.C的某一时间点同时发生,如图 10所示,其LTS语义如图 11所示.它表示在任一时刻,要么d.C与d1.C1同时tick,要么d.C与d2.C2同时tick,要么3个时钟都tick,要么3个时钟都不tick.
![]() | Fig. 10Instant graph of union图 10union的时间点图 |
![]() | Fig. 11LTS semantics of d.C![]() ![]() |
当问题领域为相同结构时,我们考虑两种时钟:一种是每个时间点都取二者最慢,一种是每个时间点都取最快,最慢的我们定义为sup,最快的定义为inf.
定义8. sup:
d.Cd1.C1 sup d2.C2.
要求d1,d2是相同结构的问题领域,问题领域d为它们的并.时钟d.C的第i个时间点与d1.C1和d2.C2的第i 个时间点中慢的一个同时发生,∀k∈,C[k]∈Id.C,如下3个关系必须满足:
3) d.C[k]≡d1.C1[k] if d2.C2[k]d1.C1[k];
d.C[k]≡d2.C2[k] if d1.C1[k]d2.C2[k].
图 12给出了其直观含义,C中的每一个时间点都取C1和C2中发生最慢的时间点.我们需要记录时钟d1.C1和d2.C2已发生过的时间点的个数的差值δ,以决定某一时刻d.C的时间点是否发生以及与谁同时发生.其LTS语义如图 13所示,当时钟d1.C1比d2.C2快时,d.C和d2.C2相应的时间点同时发生;反之,则与d1.C1对应的时间点同时发生.
![]() | Fig. 12Instant graph for sup图 12sup的时间点图 |
![]() | Fig. 13LTS semantics of d.C![]() ![]() |
定义9. inf:
d.Cd1.C1 inf d2.C2.
与sup相反,d.C的每个时间点与d1.C1和d2.C2对应时间点中较快的那个同时发生,∀k∈,C[k]∈Id.C必须满
足如下条件:
3) d.C[k]≡d2.C2[k] if d2.C2[k]d1.C1[k];
d.C[k]≡d1.C1[k] if d1.C1[k]d2.C2[k].
与其他算子类似,inf的直观含义如图 14所示,其LTS语义如图 15所示.
![]() | Fig. 14Instant graph for inf图 14inf的时间点图 |
![]() | Fig. 15LTS semantics of d.C![]() ![]() |
通过前几节的建模,得到的时间需求规约包括各种时间约束(如时间点关系约束、时钟关系约束),这些约束之间可能产生冲突.例如,某个时间点约束要求a strictPre b,而其他约束条件却推导出b strictPre a,由此产生不一致,或者时钟约束发生冲突,整个系统就会互相等待,产生死锁.靠需求分析人员手工分析各个时钟关系相互作用下所有可能的情况容易出错也不现实,因此需要形式化的方法和工具支持.由于我们已经定义了时钟、时钟关系和时钟构造算子的形式化语义,只需要找到合适的形式化工具来支持该分析.本文我们选择使用模型检测工具NuSMV来验证时间需求规约,将时间需求规约转换为NuSMV模型,用CTL公式表达要验证的性质,然后进行规约验证.
一个时间需求规约转换成一个NuSMV的FSM模型,对应一个main MODUEL(main模块),时间约束(instant relation,clcok relation,clock constructor)转换为NuSMV中的MODULE,规约中出现的时钟在main MODULE的VAR部分声明为布尔变量,出现的时钟约束创建为对应约束MODULE的实例,时钟变量的赋值对应于规约约束中,该时钟是否tick(TRUE对应tick,FALSE对应不tick).每个时钟约束的MODULE编码是其LTS语义的直接映射:状态由MODULE VAR中生命的状态变量模拟,迁移由MODUEL中TRANS constraints实现,MODULE实例共同作用,形成整个规约的FSM模型,决定规约当前的状态以及每个迁移中每个时钟的赋值.每个时钟的赋值即为当前时刻时钟的tick情况,它影响算子接下去应该处于其LTS语义中的哪一个状态.据此,得到从时间需求规约到NuSMV的转换规则,见表1.
![]() |
Table 1 Transformation rules from timing requirements specification to NuSMV models 表1 时间需求规约到NuSMV模型的转换规则 |
需要注意的是,从Instant relation到constraint MODULE的转换,常使用的时间约束大多建立在时钟层面上,而且不需要记数每个时钟的每个时间点(时钟的时间点通常无限大,记数会引入非常大的状态空间).例如, subClock不需要记数时间点而只有1个状态,fasterThan只需要记录时钟漂移δ而不是每个时间点的编号,所以我们的MODULE都实现了在时钟层面上减少状态空间.但是在这种实现框架下,时间点约束的编码需要特别处理,选出其作用的时钟的某个特定编号的时间点,所以我们引入select操作,保证时间点约束的正确实现并且尽量缩小状态空间,使NuSMV实现仍然在时钟层面上.select操作有两个参数:时钟C和整数i,select(C,k)选出时钟C的第i个时间点,select用计数器ct来记数时钟的时间点编号,直到k到达,余下的时间点将不再被记数.在时钟层面的NuSMV实现上可以理解为,select创建了一个新的虚拟时钟(这里,虚拟的意思是这个新创建的时钟没有出现在原时间规约中),该时钟只tick 1下,并且只能与时钟C的第i个时间点同时发生.
另外,由于NuSMV模型为有限状态模型,上述规则的使用必须满足一个条件:要转换的时间需求规约具有有限状态空间.有些时钟约束可能引起无界的状态空间,例如,fasterThan,sup,inf需要记录两时钟间的漂移δ.当一个时间规约含有这样的约束时,它的状态空间也可能是有限的(各个约束相互作用,使得每个漂移δ只可能落在一个有界区间内),而且大多数情况下如此.判断时间约束是否满足上面的情况(互相约束导致有界),需要额外的严格检查.
在本文中,为了避免这样的检查,我们要求如果fasterThan,sup,inf出现在一个时间规约中,对应时钟间的漂移要使用boundedDiff约束显式说明d的有界区间;而且在实际建模中,通常需求往往要求有界的差值而不是无穷大小的差值.
下面我们用一个小例子来说明上述转换规则.
表2左边给出了包含两个subClock时钟关系和一个时间点关系的时间约束,右边是其转换过去的NuSMV模型.该时间约束中的3个时钟d1.C1,d2.C2,d3.C3转换为NuSMV模型中的3个布尔变量c1,c2,c3,时钟关系subClock的LTS语义编码为MODULE subClock.如图 5所示,subClock的LTS只有1个状态,所以在MODUEL实现中不需要另外声明状态变量来模拟状态的转变,其LTS的3个迁移由TRANS中的命题公式描述.每次迁移要么两个时钟都tick,要么父时钟单独tick,要么两个时钟都不tick.规约中包含的两个subClock时钟关系在main MODULE中创建为MODULE subClock的两个实例ctr1,ctr2,时间点关系的LTS语义由instantstrictPre MODUEL实现(直接映射),它用到的两个时间点d1.C1[5]和d2.C2[3]由select(c1,5),select(c2,3)选出,对应为虚拟时钟c15,c23也声明在main MODULE的VAR里,时间点关系d1.C1[5]和d2.C2[3]<d3.C3声明为instant strictPreMODUEL的实例,与其他两个subClock的实例共同作用,决定运行中每个时钟的赋值.
![]() |
Table 2 An example of transformation 表2 转换的例子 |
CPS是感知与控制反馈循环的系统,它在环境感知的基础上,实现对物理设备的控制,如此循环往复.这样的系统应该能够保持运行,其系统时间应该持续下去.那么在CPS系统的时间需求规约中,所有时钟都应该可以再次tick.如果规约中约束具有不一致的地方,那么在规约运行中,为了保证每个时间约束都被满足,整个系统(所有时钟)或者其中的一部分(部分时钟)将不能再tick.我们称这种情况为规约存在不一致,有死锁.
由于NuSMV实现中时钟tick(不tick)表现为该时钟对应的变量赋值TRUE(FALSE),若用CTL公式来描述一致性属性,C1就表示当前状态下C1的值为1,即上一个时刻C1刚刚tick过;相反,!C1表示上一个时刻C1没有tick.规约死锁,即在某时刻起,没有时钟可以再tick,则应表述为CTL公式EF(AGp),其中,p=!(C1|C2|…|Cn)表示在某状态没有时钟tick,那么AGp表示该状态出发的所有路径中没有任何一个时钟tick.由此,我们定义全局死锁.
定义10. 对于时钟集合为T={C1,C2,…,Cn}时间需求规约,我们称该规约存在全局死锁,如果其NuSMV模型满足CTL公式EF(AGp).
由于我们假定所有时钟都应该无穷多次tick,所以如果规约运行到某点后,这个时钟永远不能再tick了,我们称这个时钟被死锁了.在系统需求分析中,某个(些)时钟对应的问题领域可能非常重要,设计者需要特别保证其不会被死锁,CTL公式提供给用户进行该检查的方法.
定义11. 对于时钟集合为T={C1,C2,…,Cn}时间需求规约,我们称该规约存在某一时钟Ci的死锁,如果其满足CTL公式EF(AGq),q=!Ci.
图 16给出了一个统一的需求建模及验证的过程,过程的输入是一个问题图,它包括问题领域、交互等等.问题图的获取过程可以参考文献[16],过程的输出是一个经过验证的时间需求规约.在图 16中有4大步,我们将使用一个案例来阐述这些步骤.其问题陈述如下:
![]() | Fig. 16The process of modeling and verifying timing requirements图 16时间需求建模验证过程 |
汽车防抱死制动系统(ABS)是一个小型的CPS系统,它的架构包含4个传感器(Sensor ifl,ifr,irl,irr)和4个执行器(Actuator ofl,ofr,orr,orl).传感器感应轮子的转动速度,执行器表征施加于轮子上的刹车压力.
ABS的执行是由R触发,且必须每5ms(最大1ms的抖动)执行一次.ABS的4个感应器的值在一定延迟内到达(也叫输入同步),输入同步延迟为0.5ms,一个类似的输出同步延迟出现在执行器.另外,它还允许从输入集合的第1个事件到最后一个输出的事件之间存在的延迟必须少于3ms.
作为过程的输入,问题图应该给出需求涉及的问题领域、交互以及领域类型(基本领域还是组合领域).
图 17给出了ABS系统的问题图,在这个图中,组合领域Sensor有4个基本领域:ifl,ifr,irl和irr.组合领域Actuator有4个基本领域:ofl,ofr,orl和orr.显然,ifl,ifr,irl,irr和Sensor是相同结构的领域,ofl,ofr,orl,orr和Actuator是相同结构的领域.
![]() | Fig. 17Problem diagram of ABS图 17ABS的问题图 |
ABS和Sensor之间、ABS和Actuator之间的交互见表3.为了简化,本文就使用intij(i可以是1,2,3,or 4,j是领域的名字)来表示子领域与ABS的交互.
![]() |
Table 3Declaration 表3 声明 |
第1步:为每个问题领域建立时钟.
这一步可以分3个子步骤来完成:
1) 为问题图中的每个问题领域声明一个时钟.在问题图中,对每个问题领域建立时钟标签.
回到我们的例子,将如图 17所示的每个问题领域加以声明,由此得到时钟声明,见表3,标上时钟,得到了带有时钟的问题图,如图 18所示.
![]() | Fig. 18Problem diagram of ABS with clocks图 18ABS带时钟的问题图 |
2) 为基本领域的时钟建模.
根据时钟的定义,这一步可以分两个子步骤来完成:
(1) 为每个时钟找到时间点.
每个时钟的时间点都是这个领域发起或者接收的交互发生的时刻,所以这一步就是去识别每个交互的发生.对问题图中的该时钟对应的问题领域的每个交互,确定其发生的时刻,标记为该时钟的时间点.
(2) 在每个时钟内确定时间点之间的严格优先关系.
确立时间点之间的严格优先关系,即,明确对应交互发生的先后顺序,可以请需求提供者进行确立.
本文例子中的基本领域包括传感器ifl,ifr,irl,irr与执行器ofl,ofr,orl,orr.int1ifl发生的时刻(记为O(int1ifl))和int2ifl发生的时刻(记为O(int2ifl))都是Cifl的时间点,因此可以有类似地,我们得到其他时钟的时间点集,见表3.
至于时间点关系,例如在时钟Cifl中,int1ifl必须发生在int2ifl之前,所以O(int1ifl)O(int2ifl).类似地,可以得到其他严格先于关系,见表3.
3) 为组合领域建模时钟.
这一步是从已有的时钟构造新的时钟,通过使用时钟构造算子来得到.对于每个组合领域,根据它与子领域的关系以及想要表达的意思,选择合适的算子来构造组合领域的时钟.若组合领域是由相同结构的领域组合而成,则可以使用sup或inf算子.若想表达最快的时钟,则用inf算子;若想表达最慢的时钟,则用sup算子.也可以选择用户自行定义的算子.若组合领域是由不同结构的领域组合而成,可以使用union算子.
在本例子中,Sensor是ifl,ifr,irl和irr的组合,而ifl,ifr,irl和irr都有相同结构的领域,而且Sensor应该表现最慢,由此得到:
Sensor.Csensor=sup(ifl.Cifl,ifr.Cifr,irl.Cirl,irr.Cirr).
类似地,可以得到:
Actuator.CActuator=sup(ofl.Cofl,ofr.Cofr,orl.Corl,orr.Corr).
第2步:确立定性关系.
第1步基本确立了同一个时钟之内的时间点关系,这一步主要是要确立时钟之间的时间点之间的关系.通常,我们确立3种关系:precedence,coincidence和strict precedence.这些时间点关系的识别还是要从对应的交互出发,请需求提供者确立发生的先后顺序.这样结合第1步,我们就可以得到所有时间点之间的定性关系,可以用时间点图表示.
在我们的例子中,在Sensor.Csensor和Actuator.CActuator之间,int2必须在int3之前发生,因此O(int2)O(int3).在Sensor.Csensor和Cifl之间,int1的发生不会早于int1ifl,所以O(int1ifl)
O(int1).
类似地,我们可以得到ABS内其他的时间点关系,如图 19所示.
![]() | Fig. 19Problem diagram of ABS图 19ABS的问题图 |
第3步:确立时间点之间的定量关系.
时间点之间的定量关系需要由需求提供者给出,定量关系首先考虑涉及到的领域、交互、时钟能否从时钟层面上给出,最后考虑时间点.一般来讲,定量相关的需求主要有3类:重复率、延迟需求以及输入输出同步.重复率型的需求一般形式是每几秒执行一次,这种类型首先考虑执行的问题领域,其对应的时钟,然后考虑filteredby时钟构造算子构造新的时钟.延迟需求和输入输出同步都是要找出执行的问题领域和交互,将领域对应的时钟分解到这个交互对应的时钟(即,时钟的时间点就是这个交互的每次发生,可以虚构).鉴于时钟的虚构性,可以仅用时钟的第1个时间点之间的定量关系来表示时间段.结合这一步得到的定量关系以及上一步得到的定性关系,我们可以得到时间需求规约.
比如,本例中重复率(repetition rate)类型的需求通常写成:ABS的功能必须每5ms(最大1ms的抖动)执行一次.这个功能通过Sensor与Actuator的组合来周期性地实现,Sensor与Actuator是不同的领域,因此,现有的时钟将是:
Sensor.Csensor union Actuator.CActuator.
根据第4节的单领域filteredby时钟构造算子,其他参数包括初始值为0,周期为5.因此,新的时钟Cnew可以通过如下算子构造出来:
ABS.Cnew(Sensor.Csensor union Actuator.CActuator)▲(1.05-1)w.
延迟需求类型的需求可以被描述为:从输入集合的第1个事件到最后一个输出的事件之间存在的延迟必须少于3ms.以Sensor的int1为例作为输入,以Actuator的int4为例作为输出,那么最初的输入为int1ifr,int1ifl,int1irl, int1irr中反应最快.由于其特殊性,我们做虚拟时钟Sensor.Cinput表示输入中最早的时钟,而为了统一,必须将原先的ifr.Cifr拆分为两个:ifr.Cifr=ifr.Cifr1 alternate ifr.Cifr2,其中,ifr.Cifr1对应交互int1ifr.其他时钟也类似,在这种情况下有:Sensor.Cinputinf(ifr.Cifr1,ifl.Cifl1,irl.Cirl1,irr.Cirr1).
最慢的输出为O(int4),为其构造虚拟时钟Actuator.CActuator2,则延迟需求表示为
Actuator.CActuator2[1]-Sensor.Cinput[1]<30.
输入输出同步型类似于需要一个0.5ms的输入同步.第1个输入是O1inf,其作为虚拟时钟Sensor.Cinput,最后的输入是O(int1),对应虚拟时钟Sensor.CSensor.于是,一个0.5ms的输入同步可以表示为
Sensor.Csensor[1]-Sensor.Cinput[1]<5.
第4步:转换为Nusmv描述进行验证.
根据第5节的转换规则,将案例时间规约转换为NuSMV模型,系统属性描述为CTL公式,我们可以检查案例时间规约的一致性,该时间规约存在全局死锁,如图 20所示.
![]() | Fig. 20Checking result: Global deadlock图 20检测结果:全局死锁 |
通过分析NuSMV提供的反例路径我们发现,该死锁是由约束CActuator2 strictPre CSensor1的不当引入造成的.在input时钟与global钟同时tick 1下后,global时钟又单独tick了5下,由约束CActuator2[1]-Cinput[1]<global5限定,下面需要时钟CActuator2 tick(与global一起),又由CActuatorCActuator1 union CActuator2得到CActuator2需要与CActuator 同时tick.时钟CActuator2和CActuator之前都没有tick过,所以CActuator的tick可以发生的条件为:之前有CSensor的第 一个时间点发生过(约束CSensor strictPre CActuator).约束CSensor
CSensor1 union CSensor2和CSensor1 strictPre CSensor2限 定CSensor的第1个时间点的发生一定要与CSensor1的第1个时间点的发生同时,所以CActuator2的第1个时间点的发生的条件为:之前CSensor1的第1个时间点发生过.这与CActuator2 strictPre CSensor1矛盾,所以规约这条路径运行到需要CActuator2 tick时发生死锁.
分析案例的需求我们发现,CActuator2 strictPre CSensor1约束应该改为CSensor2 strictPre CActuator1.我们修改了案例的时间规约,再次检查,该规约不再存在全局死锁.
基于功能性需求的时间需求建模的工作很多,例如面向目标的方法[4]和面向主体与意图的方法[5, 6]:
面向目标的方法,比如KAOS(knowledge acquisition in automated specification)[17],将目标看作是需求的来源,它使用带类型的一阶时序逻辑作为逻辑语言,既包含传统的时序算子,也包含描述涉及实时节点特性的附加实时算子,描述实时特性.它建模实时特性精确,没有显示地参考时间变量.
面向主体和意图的方法提供一种基于组织层次上下文的需求获取和建模的思路,其建模理念为刻画有目的的参与者.其代表性工作是i*框架[5]和Formal Tropos[6],它们也是采用带类型的一阶时序逻辑语言来描述时间需求.ALBERT-II(agent-oriented language for building and eliciting real-time requirements)[18]也是一种面向主体和意图的方法,它的描述基础也是一阶时序逻辑,其主体(agent)的状态和行为都通过基于逻辑的符号表示为约束.
上述工作都基于时序逻辑,时序逻辑在描述定性约束的时候没有问题.为了描述定量约束,进行了多种扩充,如Timed Computation Tree Logic[8]等,这些时序逻辑通常用于表示实时系统的性质和规范,在需求工程中用到的较多的是一阶时序逻辑和谓词时序逻辑[19].由于目标、主体与意图都不与问题领域、交互直接相关,因此上述工作都不适合建模CPS系统.
问题框架方法采用问题领域和交互进行建模,更适合建模CPS系统.在问题框架相关的时间需求比较有限, Choppy等人提出时间事件来表示时间[20],Barroca等人使用Timer作为问题领域的一部分[21].他们都没有将交互用时间显式表达出来.我们前期也做过一些基于问题框架的时间需求工程[9, 10],但是该方法侧重在多形态时间,致力于解决多样的环境时间描述与单一的软件时间描述的统一.
基于前期工作,本文提出了一种基于逻辑时钟的CPS时间需求一致性分析方法,增加了时间需求模型的形式化语法与语义,进行了不一致性属性的验证,是更深入的工作.主要贡献包括:
将逻辑时钟引入到问题框架中,构建了CPS时间需求模型.通过抽取问题框架方法与时间需求相关工作的基本概念,得到了基于问题框架的时间需求基本概念框架,为形成CPS时间需求建模机制奠定了良好的基础.
给出了CPS时间需求模型概念的语法和操作语义.通过操作语义,给出了CPS建模机制中的概念的内涵,方便了后续的形式化验证;
给出了CPS一致性时间需求验证机制.在形式化语义基础上,将时间需求规约转换成NuSMV模型,并定义了不一致性属性,使用NuSMV进行了一致性检测.通过检测,为后续的设计与实现奠定了坚实的基础.
目前,仍需要更深入的工作解决一些问题,例如,检验模型的规模偏大,如何减少检测过程中的状态空间,以加速检验的过程,如何在时钟层面上增加定量关系、自动的工具支持等等.
[1] | Lee EA. Cyber physical systems: Design challenges. In: Arlat J, ed. Proc. of the 11th IEEE Symp. on Object/Component/Service- Oriented Real-Time Distributed Computing. Washington: IEEE Computer Society, 2008.363-369 . |
[2] | Lee EA. CPS foundations. In: Proc. of the Design Automation Conf. (DAC). New York: ACM Press, 2010. |
[3] | Jackson M. Problem Frames: Analyzing and Structuring Software Development Problems. New York: Addison-Wesley, 2001. |
[4] | Van Lamsweerde A. Goal-Oriented requirements engineering: A guided tour. In: Titsworth FM, ed. Proc. of the 5th IEEE Int’l Symp. on Requirements Engineering. Washington: IEEE Computer Society, 2001.249-263 . |
[5] | Yu E. Agent orientation as a modeling paradigm. Wirtschaftsinformatik, 2001,43(2):123-132 . |
[6] | Yu E. Towards modeling and reasoning support for early phase requirements engineering. In: Agresti W, ed. Proc. of the 3rd IEEE Int’l Symp. on Requirements Engineering. Washington: IEEE Computer Society, 1997.226-235 . |
[7] | Hall JG, Rapanotti L, Jackson M. Problem oriented software engineering: Solving the package router control problem. IEEE Trans. on Software Engineering, 2008,34(2):226-241 . |
[8] | Alur R, Courcoubetis C, Dill D. Model-Checking in dense real-time. Information and Computation, 1993,104(1):2-34 . |
[9] | Chen XH, Liu J. Modeling software timing requirements: An environment based approach. Chinese Journal of Computers, 2013, 36(1):88-103 (in Chinese with English abstract). |
[10] | Mallet F, Peraldi-Frati MA, André C. Marte CCSL to execute East-ADL timing requirements. In: Werner B, ed. Proc. of the 12th Symp. on Object/Component/Service-Oriented Real-Time Distributed Computing. Los Alamitos: IEEE Computer Press, 2009.249-253 . |
[11] | André C. Syntax and semantics of the clock constraint specification language (CCSL). Research Report, 6925, INRIA, 2009. http:// hal.inria.fr/inria-00384077 |
[12] | Chen XH, Liu J, Mallet F, Jin Z. Modeling timing requirements in problem frames using CCSL. In: Thu TD, ed. Proc. of the 18th Asia-Pacific Software Engineering Conf. Washington: IEEE Computer Society, 2011.381-388 . |
[13] | Cimatti A, Clarke E, Giunchiglia E, Roveri M. NUSMV: A new symbolic model checker. Int’l Journal on Software Tools for Technology Transfer, 2000,2(4):410-425 . |
[14] | Jin Z, Chen XH, Zowghi D. Performing projection in problem frames using scenarios. In: Guerrero JE, ed.. Proc. of the 16th Asia- Pacific Software Engineering Conf. Washington: IEEE Computer Society, 2009.249-256 . |
[15] | Uchitel S, Kramer J, Magee J. Synthesis of hehavioural models from scenarios. IEEE Trans. on Software Engineering, 2003,29(2): 99-115 . |
[16] | Chen XH, Jin Z. An ontology-guided process for developing problem frame specification: An example. In: Rapanotti L, ed. Proc. of the 3rd Int’l Workshop on Applications and Advances of Problem Frames. New York: ACM Press, 2008.36-39 . |
[17] | Darimont R, van Lamsweerde A. Formal refinement patterns for goal driven requirements elaboration. In: Garlan D, ed. Proc. of the 4th ACM Symp. on the Foundations of Software Engineering. NewYork: ACM Press, 1996.179-190 . |
[18] | Bois P. The albert ii language: On the design and the use of a formal specification language for requirements analysis. [Ph.D. Thesis]. Namur: Dept. of Computer Science, University of Namur, 1995. |
[19] | Schreiber FA. Is time a real time? An overview of time ontology in informatics. Real Time ComputingSpringer Verlag NATO ASI, 1994,F(127):283-307 . |
[20] | Choppy C, Reggio G. A UML-based approach for problem frame oriented software development. Information and Software Technology, 2005,47(14):929-954 . |
[21] | Barroca L, Fiadeiro J, Jackson M, Laney R, Nuseibeh B. Problem frames: A case for coordination. In: De Nicola R, ed. Proc. of the 6th Int’l Conf. on Coordination Models and Languages. Berlin, Heidelberg: Springer-Verlag, 2004. 5-19 . |
[9] | 陈小红,刘静.基于环境的多形态时间需求建模方法.计算机学报,2013,36(1):88-103. |