随着软件本身及其运行环境的日益复杂,软件可信性问题引起人们越来越多的关注^[1].如何保证可信性涉及到软件开发过程众多方面,包括图灵奖得主A.Pnueli在内的许多计算机科学家都认为,采用形式化方法(formal method)对软件进行模型设计与验证是其中的重要手段^[2].模型检测(mode checking)^{[3, 4]}是一种验证有限状态系统满足规范的形式化方法,由于检测过程在算法支持下可以自动执行,因此被越来越多的研究者或工程人员用于对软件安全性、活性、公平性等功能属性进行可信验证.

软件模型检测主要包括3个方面的内容:一是软件建模,通过构造软件计算模型来刻画软件不同的行为特征;二是属性描述,通过时序逻辑语言(例如:计算树逻辑CTL^[5],线性时态逻辑LTL^[6],时间计算树逻辑TCTL^[7],概率计算树逻辑PCTL^[8],连续语义线性时态逻辑LTLC^[9],连续随机逻辑CSL^[10]等)定义软件必须满足的一些性质;三是检测算法,根据所使用模型的特点和时序逻辑规约设计对应的模型检测算法,这方面面临的最大问题就是状态空间爆炸,相关学者也提出了大量的解决方法,如OBDD符号化技术^[11]、组合验证^[12]、界限模型检测^{[13, 14, 15]}等.

在软件建模方面,可采用形式化模型和半形式化模型.形式化模型主要是自动机、Petri网以及它们的相关扩展模型^{[16, 17, 18]}.形式化模型的优势在于本身具有严格的数学规范,可直接用于模型检测;缺点在于模型难以理解,不利于软件开发人员进行后续软件开发.半形式化模型主要为UML及其扩展模型^{[19, 20]},其优势在于可直接用于软件开发;其缺点是不能直接进行模型检测,需要进一步转化为形式化模型.在这个过程中,也缺少自动化工具支撑,所以实用性较差.

针对上述问题,日本CASE株式会社提出了一种基于STM的软件建模方法,并已开发出商用工具ZIPC^[21],目前已在嵌入式软件开发领域得到了广泛应用.在STM中(如图 1所示),列表示软件中存在的状态;行表示软件中将要发生的事件;行列交叉单元表示在某一状态下,当某一事件发生时,软件需要进行的处理.处理包括两部分内容:一是正常的事务处理,二是软件状态迁移.通过STM结构,既保留了软件模型的形式化语义,又便于后续软件开发(软件需求、设计均可通过STM完成,并且可以自动生成软件代码框架).STM支持层次化设计,可将大型软件分解为若干子系统,各子系统由若干STM表格组成,各表格之间可通过共享变量、消息传递或者表格调用等机制进行通信.此外,STM还可以显式地表示出软件设计遗漏(使用图 1中的“错误(x)”单元和“忽略(/)”单元,例如:在电源ON状态下,发生了ON事件该如何处理;在电源OFF状态下,发生了OFF事件该如何处理),这些遗漏对于软件安全性影响较大,而通过传统的软件建模方法难以被有效地发现.

目前,针对软件STM模型的正确性验证包括两种方法:一种是通过动态仿真运行,实时观测STM的事务处理与状态迁移是否满足软件设计要求,另一种是使用模型检测手段,将STM模型与待验证的软件属性编码为一阶谓词逻辑公式,通过模型验证工具验证软件设计是否满足属性要求^{[22, 23]}.

作为一种实用性较强的软件建模方法,STM也存在一定的问题.主要体现在建模手段上,无法有效地表示事务处理时间,进一步导致了系统状态迁移时间不能被有效分析.而嵌入式软件对实时性要求严格,因此,通过STM无法分析嵌入式软件时间特性.针对这一问题,本文提出了一种TSTM的形式化建模方法,通过为各单元操作引入时钟映射函数,使TSTM具有显示表示时间的能力.此外,针对TSTM,给出了一种基于BMC策略的TCTL模型检测方法,用以验证TSTM时间及逻辑属性.最后,通过TSTM,对某型号列控制软件进行建模与验证,证明上述方法的有效性.

1TSTM与TCTL相关定义 1.1TSTM形式化定义

在给出TSTM形式化定义之前,首先定义TSTM建模语言L.L语言是ANSI-C语言的一个子集,它遵从C语言的语法和语义.L语言数据类型域由布尔型(Boolean)、整数型(integer)和实数型(real)组成,支持的表达式包括:(1) 布尔文字{true,false}、整数文字和实数文字;(2) 变量标识符;(3) 中缀表达式:{expression 1}操作符{expression 2},其中,操作符包括+,-,*,/,&&,||,!=,=.L支持的语句包括:(1) 赋值语句stl=str;(2) 条件判断语句if {condition}{statement 1} else {statement 2};(3) 分支判断语句switch {condition}, case 1 {statement 1}; … case n {statement n}.

定义1(TSTM). 一个TSTM表格H可以用五元组áS,E,C,T,Fñ表示,其中,

· S是有限状态集合.每个状态sÎS都有唯一的自然数索引值index(s)ÎN与之相对应.在H运行过程中,只有唯一的激活状态,用active(H)表示.初始时,默认激活状态s的索引值index(s)=0(即最左侧状态).

· E是有限事件集合.包括外部事件E_external和内部事件E_internal,且E_externalÇE_internal=Æ.每个外部事件e_XÎE_external用L的一个布尔变量表示;每个内部事件e_IÎE_internal用L的一个布尔表达式或布尔变量表示.每个状态eÎE都有唯一的自然数索引值index(e)ÎN与之相对应.

· C是有限单元集合,包括正常单元C_normal、忽略单元C_ignore和错误单元C_error(也称为不可用单元):

(1) 正常单元c_NÎC_normal是一个六元组ás,e,u,a,s¢,jñÎSxEx(LÈI(X)È{& lt; i>null})x(LÈ{/})xSxF,其中, source(c_N)=s为c_N所对应的状态,event(c_N)=e为触发c_N的事件,guards(c_N)=u为守卫条件(包括逻辑条件与时间约束),actions(c_N)=a为执行动作,target(c_N)=s¢为迁移目标状态,F(c_N)=j为执行时间赋值,I(X)为时钟约束集,文字null表示无守卫条件.单元c_N规定了当H处在状态source(c_N)且有事件event(c_N)到来,当满足guards(c_N)中的逻辑条件和时间约束时,H的动作行为actions(c_N)以及对应的执行时间消耗F(c_N).

(2) 忽略单元c_IÎC_ignore是一个三元组ás,e,/ñ,其中,s,e定义与c_N相同,符号“/”表示什么都不做.

(3) 错误单元c_EÎC_error是一个三元组ás,e,×ñ,其中,s,e定义与c_N相同,符号“×”表示发生错误.

· T是有穷时钟集合,X为时钟变量集合,时钟约束d的集合I(X)={d|d::=x≤a|a≤x|Ød|d₁Ùd₂},其中,x是X中的一个时钟,a是非负有理数集Q中一个常量.

· F是时钟映射函数,它为TSTM中每个正常单元c_NÎC_normal指定F(c_N)ÎT中某个时钟赋值.时钟集合T上的时钟赋值是指为每个时钟分配一个实数值,也可以说它是从集合T到非负实数集R的一个映射.T上一个时钟赋值满足X上一个时钟约束d,当且仅当依照时钟赋值给出的时钟值,时钟约束d的布尔值为真.

1.2TCTL语法与语义

TCTL是在CTL基础上,通过在时态逻辑算子上增加时间约束实现对实时系统时间属性的刻画.下面给出TCTL的语法和语义.

定义2(s-路径). 对于状态集合S和sÎS,通过S的s-路径是从R到S满足r(0)=s的映射r.

定义3(TCTL结构). TCTL结构是三元组M=ás,m,fñ,其中,

· S是状态集合;

· m:s®2^AP是一个标记函数,AP为原子命题集合,m赋给每一个状态原子命题集合为真;

· f是给定每一个sÎS一通过S的s-路径集合的映射.

定义4(TCTL公式). a,b::=true|p|Øa|aÙb|aÚb|EF_ja|EaU_jb|AaU_jb,其中,p是原子公式,jÎR⁺是时间约束,包含以下形式:[n,m],[n,m),(n,m],(n,m),[n,¥]和(n,¥),n,mÎN.

定义5(TCTL语义). 对于TCTL结构M=ás,m,fñ,令s_iÎS,pÎAP,pÎf(s_i)是以s_i为起始状态的s-路径,y为TCTL公式,则满足关系(M,s_i)y可定义如下:

· s_ip当且仅当pÎm(s_i);

· s_iØp当且仅当pÏm(s_i);

· s_iaÙb当且仅当(s_ia)Ù(s_ib);

· s_iaÚb当且仅当(s_ia)Ú(s_ib);

· s_iEF_ja当且仅当

· s_iEaU_jb当且仅当

· s_iAaU_jb当且仅当

这里,用I_j表示时间约束j被满足,用表示状态i满足时间约束j.

1.3TSTM动态行为及全局状态空间构造

一个软件设计D通常由多个TSTM H₁,H₂,…,H_n组合而成,即D=(H₁,H₂,…,H_n).软件运行时,这些TSTM内部状态将进行迁移,TSTM间全局共享变量将发生变化,这些状态和全局变量变化即为软件D的状态迁移.

定义6(TSTM动态行为). 用TSTM建模的软件设计D,其动态行为可以定义为B(D)=áG,g_init,Dñ,其中,

· G为全局状态集合,包含了各TSTM的激活状态active(H₁),active(H₂),…,active(H_n)以及D中所有变量X(D)的当前取值value(X(D)).即,G=áactive(H₁),active(H₂),…,active(H_n),value(X(D))ñ.

· g_init为初始状态.在初始状态,TSTM H_i的激活状态s_i满足index(s_i)=0,变量x_iÎX(D)为初始默认值.

· 为状态迁移,即,当TSTM H_i的c_NÎC_normal类型单元格运行时(使能),全局状 态G将发生迁移.用enabled(c_N,g)表示c_N在全局状态g下使能,当且仅当以下条件都为真:

(1) 单元c_N的对应状态是H_i的激活状态active(H_i)=source(c_N);

(2) 在全局状态g下,触发c_N的事件发生event(c_N,g)=true;

(3) 在全局状态g下,c_N的守卫条件满足guards(c_N,g)=true.

当单元c_N使能时,action(c_N)表示的操作语句将自动执行,使软件设计D从全局状态g迁移到另一个全局状态g¢,用ág,c_N,g¢ñÎD表示,并且在下一个状态g¢中,H_i的激活状态active(H_i)=target(c_N).

给定一个软件设计D及其动态行为B(D),则一条执行序列sq可表示为g₀,g₁,…,g_n,其中,g₀=g_init,对任意iÎN, ág_i,c_N,g_i+1ñÎD.全局可达状态为包含在与动态行为B(D)相关任何执行序列中的状态,所有全局可达状态集合用R_B(D)表示.因此,要描述一个软件属性f:G®Boolean在B(D)的所有全局可达状态得到满足,可表示为

"g:R_B(D)×f(g).

2 基于BMC技术的TSTM验证方法

BMC技术是针对OBDD符号模型检测不足而产生的一种新的模型检测技术^{[24, 25, 26]},其基本思想是在整数界限为k长度之内的执行路径中,寻找不满足性质的反例(counter-example).BMC的优势就是把BMC问题编码成SAT^[27]/SMT^[28]实例,并充分利用已有验证工具进行求解,使可验证的系统规模和变量数得到较大的提升.目前的SAT/SMT求解器^{[27, 29]}可以处理具有几千个变量的公式,保证了BMC方法的有效性.此外,由于BMC采用广度优先搜索策略,因此所获得的反例长度最短、最简明,有利于理解和找出违反性质的原因.

2.1 针对TSTM的BMC方法

基于BMC技术的TSTM模型验证方法如下:

(1) 将待验证软件建模为TSTM模型,并构造其全局可达状态集合构成的有限自动机模型M.

(2) 设验证边界上界k,用TCTL公式表示待验证软件属性的否定形式(negative normal form,简称NNF)f.

(3) 将模型M和待验证属性的NNF形式进行合取,构成k步之内的BMC公式:

其中,表示第k步时M的执行序列(s₀为起点),表示第k步时的属性表达式.

(4) 将BMC公式求解问题规约为逻辑公式的可满足性判定,即,转化为SAT/SMT实例,然后通过求解工具自动判定.若判定结果可满足,则找到反例;若不可满足,则表明待验证属性在软件运行到k阶段以内是成立的.

2.2 符号编码方法 2.2.1 TSTM符号编码方法

文献^{[22, 23]}针对STM模型给出了符号化编码方案,在此基础上,由于TSTM为c_NÎC_normal增加了执行时间赋值F(c_N),因此可以计算状态迁移过程中累计时间消耗.分析此类问题时,软件TSTM模型中需增加时间变量.此外,对于时间敏感的状态迁移,也需在guards(c_N)判定中增加对应的时间约束判定.在采用BMC技术对TSTM进行符号化编码时,设模型检测边界为bd,令0≤k≤bd,在第k步的变量和时间累积分别使用x[k]和time[k]表示.

B(D)的初始状态用step[0]表示,公式如下:

其中,value(X(D)[0])表示所有全局变量的初始值,active(H_i)[0]表示TSTM H_i的初始状态,time[0]表示系统的初始时间.

(1) 单元格c_N的符号编码方法

在TSTM中,模型状态迁移是由于c_NÎH_i.C_normal的执行,即,正常单元格被触发.为了得到B(D)在第k步的状态公式step[k],需要给出第k步时c_N的使能条件:

enabled(c_N)[k]=guards(c_N)[k-1]Ùevent(c_N)[k-1]Ùactive(H_i)[k-1]=source(c_N).

其中,guards(c_N)[k-1]表示在第k-1步时c_N守卫条件,event(c_N)[k-1]表示在第k-1步时能够触发单元格c_N执行的事件,active(H_i)[k-1]表示在第k-1步时TSTM H_i的激活状态,source(c_N)表示单元格c_N所对应的状态.

当c_N满足运行条件(被使能后)时,就需运行c_N中相关操作,则在第k步c_N执行的操作可编码为

effects(c_N)[k]=actions(c_N)[k]Ùactive(H_i)[k]=target(c_N)Ùtime[k]=time[k-1]+F(c_N).

action(c_N)[k]表示c_N中相关操作(具体编码方案可见文献^[22]),即,事务处理或变量赋值;active(H_i)[k]表示在第k步时TSTM H_i的激活状态,这个状态为c_N对应的迁移目标状态target(c_N) ;time[k]=time[k-1]+F(c_N)表示更新模型运行时间,因为c_N运行需要消耗时间,通过这一操作实现动态行为B(D)的时间累计.

最后,单元格c_N可符号编码为

x[k]=x[k-1]表示由于c_N的使能条件没有满足,因此第k步的变量取值与第k-1步相同.

(2) 事件e的符号编码方法

在TSTM中,模型状态迁移需要通过事件进行触发,事件又分为内部事件和外部事件:内部事件由c_N的运行而触发,外部事件需要由与模型交互的环境触发.下面给出当外部事件e触发时模型需要进行的处理:

其中,e[k]表示第k步时的事件状态,为布尔型变量.

(3) 第k步step[k]符号编码方法

通过c_N[k]和ext(e)[k]的编码方法,可以得到软件TSTM模型动态行为B(D)在第k步时的符号编码方法:

2.2.2 TCTL属性编码方法

针对TCTL的界限模型检测,相关学者已给出了BMC编码及优化方案.本文采用文献^[13]的符号编码方法,下面给出TCTL的边界语义.

定义7(TCTL边界语义). 令M_k为模型M的第k步时的转换公式,s_iÎS,pÎAP,a,b为TCTL公式的否定形式(NNF),M_k,s_ka表示在状态sÎM_k中a为真.则_k可定义如下:

· M_k,s_kp当且仅当pÎm(s);

· M_k,s_kØp当且仅当pÏm(s);

· M_k,s_kaÙb当且仅当(M_k,s_ka)Ù(M_k,s_kb);

· M_k,s_kaÚb当且仅当(M_k,s_ka)Ú(M_k,s_kb);

· M_k,s_kEF_ja当且仅当

· M_k,s_kE(aU_jb)当且仅当

· M_k,s_kA(aU_jb)当且仅当

其中,p=w₀,…,w_k为模型M在第k步时路径公式,(w_i,w_i+1)ÎT,T为模型中的迁移.

在得到TSTM和TCTL的BMC公式之后,即可进行模型检测.设需要验证的软件属性为f,则在bd步之内验证系统设计D是否满足性质f的BMC公式为

3 实验分析

下面以某型号列车控制系统周期通信环节和站台门联动控制通信过程为例来说明本文方法的实用性,其中,ATP代表列车,CCS代表控制中心系统.

3.1 列控系统TSTM模型设计

ATP与CCS周期通信过程如图 2所示.

具体通信流程如下:

(1) CCS第1次接收到ATP应答器在管辖范围内的M136消息包后,若此前没有向该车发送过配置参数,则立即向该ATP发送M24+P3消息包.

(2) 当CCS检测到ATP注册完毕后,以T_ATP=6s为周期,固定向ATP发送M24消息包;同时,ATP应按T_ATP周期向CCS发送M136消息包;通信双方若超过T_ATP时间未收消息包,则内部报警.

(3) 当CCS接收到CTC设备(调度控制系统)发送的列车运行计划或折返命令时,将在M24消息包中加入CTCS-21包(运行计划)或CTCS-22包(折返命令).

(4) CCS在接收到ATP发送的CTCS-26(车载状态包)后,应转发给CTC设备.

在ATP与CCS周期通信过程中,会发生站台门联动控制通信过程,如图 3所示.具体控制流程如下:

(1) CCS根据ATP发送的CTCS-24中开门侧信息和股道(站内岔道)信息,计算出所要控制的屏蔽门侧信息:当股道为偶数时,屏蔽门在列车左侧;当股道为奇数时,屏蔽门在列车右侧.

(2) 当CCS检测到ATP发送的CTCS-24中站台编号不在CCS管辖范围内时,CCS应注销列车.

(3) 当CCS检测到ATP发送的CTCS-24中开门侧命令与CCS配置门侧信息不一致时,CCS应注销列车.

(4) CCS应仅在接受CTCS-24中的股道编号和门侧信息正确后,才能向TCC(技术控制中心)发送更新后的屏蔽门开关命令.

(5) CCS在收到ATP发送的开门命令(CTCS-24包)后,判断屏蔽门状态,若变为开门状态,则立即向ATP回复CTCS-23屏蔽门状态数据包.

(6) CCS在收到ATP发送的关门命令(CTCS-24包)后,判断屏蔽门状态,若变为关门状态,则立即向ATP回复CTCS-23屏蔽门状态数据包.

在明确上述建模需求后,即可对其进行TSTM建模.由于CCS负责与ATP进行周期通信以及车门与站台门联动控制通信,因此逻辑较为复杂.若采用单一TSTM表格进行设计,则表格过大.因此,针对CCS采用层次化TSTM建模方法,将CCS功能建模为3个表:CCS表(父表ZEH_0)、CYCLE表(子表ZEH_0.1)和DOORSCTRL表(子表ZEH_0.2).其中,

· CCS表负责接受ATP的M136消息包(如图 4所示)以及CTC设备的运行控制指令,除ATP注册功能由自身实现外,其余各事件的处理均由CYCLE表和DOORSCTRL表完成;

· CYCLE表负责完成CCS与ATP的周期通信(如图 5所示);

· DOORSCTRL表负责完成车门与站台门联动控制通信(如图 6所示).

ATP所有功能均由ATP表实现(如图 7所示),包括ATP启动、处理CCS发送的M136消息包事件以及处理车门开关事件.

TSTM为每个可以正常运行的单元格增加时间赋值F(c_N),用于表示c_N内部所有操作的时间之和.在本实验各TSTM模型中,事件和状态的含义见表 1和表 2.

各单元格进行的事务处理请见TSTM中函数名,这里不再额外进行解释.此外,为压缩TSTM表格规模,默认下述3种情况不在表中画出:(1) 在TSTM模型中的事件(布尔型,事件发生为true)均由其对应的c_N进行置false操作;(2) 在M24和M136消息包周期发送过程中,凡由发送方置true的逻辑事件或者处理,均由接收方进行置false处理;(3) 对于CCS表和ATP表,均可通过外部事件触发(关闭动作)返回OFF(CCS)或IDLE(ATP)状态.

3.2 列控系统TSTM模型验证

对于TSTM模型,有4类属性需要进行验证,这些属性对于TSTM模型可靠性来说都是至关重要的.

(1) 错误单元格的不可达性

在TSTM中,错误单元格是指在某一状态下不应该发生的特定事件所对应的单元格,即模型中标记为“×”的单元格.有两个原因会导致系统进入错误单元格:一个是该单元格本应该为普通单元格,即c_NÎC_normal,但由于模型设计人员失误将其标记为错误单元格;另一个是该单元格本身应为错误单元格,但由于系统设计错误,在该单元格对应状态下发生了不该触发的事件,使TSTM模型运行进入到错误单元格.上述两种情况都应该避免出现,因此,在TSTM模型检测中需要对其进行验证.我们用active(H,g)表示在全局可达状态g中TSTM H的当前激活状态,对于TSTM H_i的错误单元格不可达属性可以表示为

"c_EÎH_i.C_error,"gÎR_B(D),Ø((active(H_i,g)=source(c_E))Ù(event(c_E,g)=true)).

在本例中,有6个单元格为错误单元格,这里用Cell(index(s),index(e))去标识单元格位置,它们分别是CCS表的Cell(1,0)、DOORSCTRL表的Cell(1,0)和Cell(0,1),ATP表的Cell(1,0),Cell(0,2)和Cell(0,3).通过观察上述单元格可以发现:DO ORSCTRL表的Cell(1,0)和Cell(0,1)是由内部事件触发,需要进行不可达性分析;而其他错误单元均为外部事件触发,这里可以不做分析(外部事件不受系统内部行为约束,因此可以随时触发,由其引发的错误单元格是可达的.若将与本模型交互的外部系统也进行整体建模,则这些事件将变为内部事件,由它们引发的错误单元不可达性就需要进行分析).

DOORSCTRL表的Cell(1,0)表示站台门已处于开门状态,而CCS又接收到ATP开门请求;DOORSCTRL表的Cell(1,0)表示站台门已处于关门状态,而CCS接收到ATP关门请求.这两条属性可以表示为:

· Unreachability=Ø((CTCS24_Open=true)ÙDoorOpen(DOORSCTRL));

· Unreachability=Ø((CTCS24_Closs=true)ÙDoorCloss(DOORSCTRL)).

(2) 静态属性

静态属性是指不同TSTM模型之间存在某种相关性,这种相关性可以表述如下:如果TSTM A处于状态s_a,则可以推断出TSTM B处于(或者不处于)状态s_b,可以表示为如下公式:

"gÎR_B(D),active(H_A,g)=s_aÞactive(H_B,g)=s_b.

当TSTM模型规模较小时,这类问题看似容易解决;但当模型规模较大时,设计人员就很难从全局掌握这类静态属性.在本例中,我们分析如下几条静态属性(下列蕴含公式的前置条件已在本模型中验证为真):

· Static 1=IDLE(ATP)ÞWAIT_CMD(CCS);

· Static 2=WAIT_CMD(ATP)ÞWAIT_CMD(CYCLE);

· Static 3=WAIT_CMD(ATP)ÞDoorOpen(DOORSCTRL);

· Static 4=IDLE(ATP)ÞDoorOpen(DOORSCTRL).

Static 1表示当ATP处于未运行状态时,CCS处于等待命令状态;Static 2表示当ATP处于等待命令状态时, CYCLE也处于等待命令状态;Static 3表示当ATP处于等待命令状态时,DOORSCTRL处于联动门开门状态; Static 4表示当ATP处于未运行状态时,DOORSCTRL处于联动门开门状态.

(3) 动态属性

动态属性是指当一个TSTM模型状态发生变化时,另一个TSTM模型处于某个特定状态.即,当TSTM模型

A从状态s_a迁移到后,TSTM模型B应该处于状态s_b,可以表示为如下公式:

这类属性当TSTM模型规模较大时也很难直接观察到,因此需要进行模型检测验证这类问题.在本例中,我们分析如下几条动态属性:

· Dynamic 1=IDLE(ATP)®WAIT_CMD(ATP)ÞDoorOpen(DOORSCTRL);

· Dynamic 2=IDLE(ATP)®WAIT_CMD(ATP)ÞWAIT_CMD(CCS);

· Dynamic 3=DoorCloss(DOORSCTRL)®DoorOpen(DOORSCTRL)ÞWAIT_CMD(ATP).

Dynamic 1表示当ATP由未运行状态迁移到等待命令状态后,DOORSCTRL处于联动门开门状态;Dynamic 2表示当ATP由未运行状态迁移到等待命令状态后,CCS处于等待命令状态;Dynamic 3表示当DOORSCTRL由联动门关状态迁移到联动门开状态后,ATP处于等待命令状态.

(4) 逻辑及时间属性

TSTM模型中存在大量逻辑事件,各单元格内部又包含着各类事务处理,这些事件之间、事务处理之间以及事件与事务处理之间存在着逻辑相关性.例如在本例中,当ATP的xDoorOpen事件触发时,DOORSCTRL表中的sendOpenCMDtoTCC(×)函数将执行.但在逻辑验证中,我们只关心sendOpenCMDtoTCC(×)函数是否发生,因此可将其定义为布尔型变量,再进行相关验证.在本例中,可以验证如下逻辑属性:

· Logic 1=EF(xDoorOpen==true®sendOpenCMDtoTCC==true);

· Logic 2=EF((M136==trueÙCTCS23=true)®(M24==true)).

Logic 1属性含义为:当事件xDoorOpen发生时,是否存在执行路径使sendOpenCMDtoTCC(×)函数执行; Logic 2属性含义为:当CTCS23加入到M136消息包时,是否存在执行路径使CCS发送M24消息包.

此外,时间属性也需要进行验证,这对于嵌入式软件和通信类软件尤为重要.TSTM为每个c_NÎC_normal增加一个时间赋值F(c_N)用于记录单元格内所有操作的消耗时间.这个时间可由模型设计人员根据建模需求直接给出,也可根据单元格内操作复杂程度进行估算(此时,具体操作内容需完整给出.例如,函数sendOpenCMDtoTCC(×)需要给出其函数体代码).在正确标记F(c_N)后,验证时间属性时需要在各c_N中增加语句time=time+F(c_N)实现状态迁移时间累计.

目前,可以验证两个方面的时间属性:一是周期性事件到达时间是否满足时间约束,二是系统状态从g迁移到g¢是否满足时间约束(g,g¢ÎR_B(D)为任意两个全局可达状态).在本例中,可以验证如下时间属性:

· Time 1=EF_(0,6](M24==true®M136==true);

· Time 2=EF_(0,50]((M136==trueÙP44_CTCS26_Log==true)®(sendM136toCTC=true)).

Time 1表示在时间约束小于等于6秒的情况下,是否存在一条执行路径使得当M24消息包触发时,M136消息包也将被触发;Time 2表示在时间约束小于等于50s的情况下,是否存在一条执行路径使得当P44_ CTCS26_Log加入M136消息包并且被发送时,事物处理SendM136toCTC将被执行.

下面可通过第2节提出的符号编码方法对上述实例进行编码,把生成的BMC逻辑公式转化为SMT-LIB 2.0公式,并使用Z3 v4.3.2(http://z3.codeplex.com/releases)对上述实例属性进行验证,运行环境为(Windows 7 64bit, 2.8GHz,8GB RAM).附录中给出了TSTM模型的部分SMT-LIB 2.0公式.为了验证本方法的实用性,我们使用UPPAAL^[30]对列控系统需求进行重新建模(如图 8、图 9所示,这里,CCS不需要层次化设计),并验证上述属性(属性需改写为UPPAAL表示形式),对比结果见表 3.

在验证过程中,我们引入一些错误属性来检验本文方法的有效性.实验结果见表 3,属性Static 4及Dynamic 1的否定形式经判定为sat,说明这两个属性在本TSTM模型中不可满足(这两个属性是根据软件规约设计出的错误属性.在实际建模时,要检测模型设计是否存在问题,因此,通过设计满足软件规约的属性,使用本方法可以检测出TSTM模型存在 的问题).如果实验结果输出为unsat,则可增加有界模型检测步数k直到输出结果为sat或达到预先设定的检测步数最大值K(本例中为50).如果满足,说明在k步之内找到了一个反例,则该模型被检测出设计漏洞或错误.模型检测工具可以返回一个反例,通过对反例的解读,可以得到性质不成立的原因,为模型修正提供重要线索;反之,如果SMT实例不可满足,则表明待验证系统模型运行到k阶段时是安全的、没有错误的.

从验证效率来看,在现有模型规模下,本文的验证方法效率与UPPAAL相当(UPPAAL采用了多种优化策略),对不可满足属性验证时间消耗小于UPPAAL.从验证能力来看,UPPAAL无法验证错误单元不可达性,原因在于软件建模时,UPPAAL无法表示TSTM中不可达单元,此外,部分属性也无法通过UPPAAL表示(例如属性Time 2).TSTM状态与事件交叉组合出软件所有可能执行情况,这对软件开发阶段查找需求与设计遗漏非常重要,从这个角度来看,带有时间约束的TSTM建模能力要优于UPPAAL,同时也更便于软件开发人员理解与使用.

4 总结与展望

STM已广泛应用于嵌入式软件开发,但由于缺乏时间语义,限制了其建模能力.针对这一问题,本文提出了一种TSTM形式化建模方法,给出了TSTM形式化定义,通过为各单元操作引入时间映射函数和时间约束,使TSTM具有显示表示时间问题的能力.此外,针对TSTM模型验证,给出了基于TCTL的BMC模型检测方法,并通过实验证明了建模与验证方法有效性.在未来的工作中,还有几个方面的工作需要进一步研究:一方面,TSTM建模与验证过程中,c_N执行不可被中断.未来将研究c_N执行可被中断的情况,这更符合嵌入式软件特点.但时间属性验证也更为困难,因为这种情况下F(c_N)是非确定的.另一方面,未来将在文献^{[22, 23]}的基础上进一步研究TSTM符号编码优化方法,提高模型验证效率.

致谢        感谢论文评审专家中肯而有益的评审意见和相关编辑严谨、热情的工作;感谢孔维强教授在论文撰写过程中提供的耐心指导与帮助.

附 录

模型中的变量:所有事件(布尔型)、单元格中的变量(实型或布尔型)以及单元格中的函数(验证时转为布尔型,因为只需验证其是否发生).TSTM模型的部分SMT-LIB 2.0公式如下:

(set-logic QF_RDL)

(set-info :smt-lib-version 2.0)

;;;;; initial state information

(declare-fun x0_0 (×) Bool)

(declare-fun x1_0 (×) Bool)

//省略部分定义…

(declare-fun x38_0 (×) Real)

(declare-fun x39_0 (×) Real)

(assert (and (not x0_0) (not x1_0) (not x2_0) (not x3_0) (not x4_0) (not x5_0) (not x6_0) (not x7_0) (not x8_0) (not x9_0) (not x10_0) (not x11_0) (not x12_0) (not x13_0) (not x14_0) (not x15_0) (not x16_0) (not x17_0) (not x18_0) (not x19_0) (not x20_0) (not x21_0) (=x22_0 0) (not x23_0) (=x24_0 0) (not x25_0) (not x26_0) (not x27_0) (not x28_0) (=x29_0 0) (=x30_0 0) (=x31_0 0) (not x32_0) (not x33_0) (not x34_0) (not x35_0) (=x36_0 0) (=x37_0 0) (=x38_0 0) (=x39_0 0)))

;;;;; variables at step 1

;;;;; step variable information

(declare-fun x0_1 (×) Bool)

(declare-fun x1_1 (×) Bool)

//省略部分定义…

(declare-fun x38_1 (×) Real)

(declare-fun x39_1 (×) Real)

(declare-fun BoundTaskStm_1 (×) Real)

(declare-fun TranIDStatusEvent_1 (×) Real)

;;;;; assumptions at step 1 (省略部分公式)

(assert (or (and (=x28_0 false) (=x0_1 x0_0) (=x1_1 x1_0) (=x2_1 x2_0) (=x3_1 x3_0) (=x4_1 x4_0) (=x5_1 x5_0) (=x6_1 x6_0) (=x7_1 x7_0) (=x8_1 x8_0) (=x9_1 x9_0) (=x10_1 x10_0) (=x11_1 x11_0) (=x12_1 x12_0) (=x13_1 x13_0) (=x14_1 x14_0) (=x15_1 x15_0) (=x16_1 x16_0) (=x17_1 x17_0) (=x18_1 x18_0) (=x19_1 x19_0) (=x20_1 x20_0) (=x21_1 x21_0) (=x22_1 x22_0) (=x23_1 x23_0) (=x24_1 x24_0) (=x25_1 x25_0) (=x26_1 x26_0) (=x27_1 x27_0) (=x28_1 true) (=x29_1 x29_0) (=x30_1 x30_0) (=x31_1 x31_0) (=x32_1 x32_0) (=x33_1 x33_0) (=x34_1 x34_0) (=x35_1 x35_0) (=x36_1 x36_0) (=x37_1 x37_0) (=x38_1 x38_0) (=x39_1 x39_0) (and (=BoundTaskStm_1 1025) (=TranIDStatusEvent_1 0))) (and (=x27_0 false) (=x0_1 x0_0) (=x1_1 x1_0) (=x2_1 x2_0) (=x3_1 x3_0) (=x4_1 x4_0) (=x5_1 x5_0) (=x6_1 x6_0) (=x7_1 x7_0) (=x8_1 x8_0) (=x9_1 x9_0) (=x10_1 x10_0) (=x11_1 x11_0) (=x12_1 x12_0) (=x13_1 x13_0) (=x14_1 x14_0) (=x15_1 x15_0) (=x16_1 x16_0) … (=x19_1 x19_0) (=x20_1 x20_0) (=x21_1 x21_0) (=x22_1 x22_0) (=x23_1 x23_0) (=x24_1 x24_0) (=x25_1 x&l t;/ i>25_0) (=x26_1 x26_0) (=x27_1 x27_0) (=x28_1 x28_0) (=x29_1 x29_0) (=x30_1 x30_0) (=x31_1 x31_0) (=x32_1 x32_0) (=x33_1 x33_0) (=x34_1 x34_0) (=x35_1 x35_0) (=x36_1 x36_0) (=x37_1 x37_0) (=x38_1 x38_0) (=x39_1 x39_0) (and (=BoundTaskStm_1 1025) (=TranIDStatusEvent_1 4)))))

;;;;; property variable at step 1

(declare-fun loop1 (×) Bool)