模型惠普z800

软件学报ISSN1000-9825,CODENRUXUEWE-mail:jos@iscas.
ac.
cnJournalofSoftware,2015,26(8):19681982[doi:10.
13328/j.
cnki.
jos.
004689]http://www.
jos.
org.
cn中国科学院软件研究所版权所有.
Tel:+86-10-62562563一个命题投影时序逻辑符号模型检测器逄涛1,2,段振华1,2,刘晓芳1,21(西安电子科技大学计算理论与技术研究所,陕西西安710071)2(综合业务网理论与关键技术国家重点实验室(西安电子科技大学),陕西西安710071)通讯作者:段振华,E-mail:zhduan@mail.
xidian.
edu.
cn摘要:现有模型检测工具的形式化规范语言,如计算树逻辑(computationtreelogic,简称CTL)和线性时序逻辑(lineartemporallogic,简称LTL)等的描述能力不足,无法验证ω正则性质.
提出了一个命题投影时序逻辑(propositionalprojectiontemporallogic,简称PPTL)符号模型检测工具——PLSMC(PPTLsymbolicmodelchecker)的设计与实现过程.
该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模型检测算法.
PLSMC的规范语言PPTL具有完全正则表达能力,这使得定性性质和定量性质均可被验证.
此外,PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题.
最后,利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证.
实验结果表明,PPTL符号模型检测工具扩充了NuSMV系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证.
关键词:符号模型检测;时序逻辑;模型检测器;嵌入式系统验证中图法分类号:TP181中文引用格式:逄涛,段振华,刘晓芳.
一个命题投影时序逻辑符号模型检测器.
软件学报,2015,26(8):19681982.
http://www.
jos.
org.
cn/1000-9825/4689.
htm英文引用格式:PangT,DuanZH,LiuXF.
Symbolicmodelcheckerforpropositionalprojectiontemporallogic.
RuanJianXueBao/JournalofSoftware,2015,26(8):19681982(inChinese).
http://www.
jos.
org.
cn/1000-9825/4689.
htmSymbolicModelCheckerforPropositionalProjectionTemporalLogicPANGTao1,2,DUANZhen-Hua1,2,LIUXiao-Fang1,21(InstituteofComputingTheoryandTechnology,XidianUniversity,Xi'an710071,China)2(StateKeyLaboratoryofIntegratedServicesNetworks(XidianUniversity),Xi'an710071,China)Abstract:Theformalspecificationlanguagesforexistingmodelcheckingtoolssuchascomputationtreelogic(CTL)andlineartemporallogic(LTL)arenotpowerfulenoughtodescribeω-regularproperties,inthatthosepropertiescannotbeverifiedwiththem.
Inthisstudy,adesignandimplementationprocedureofpropositionalprojectiontemporallogic(PPTL)symbolicmodelchecker(PLSMC)isdevelopedbyimplementingthesymbolicmodelcheckingalgorithmforPPTLfromauthor'spreviousworkbasedontheacclaimedsymbolicmodelcheckingsystemNuSMV.
AsPPTLhastheexpressivepoweroffull-regularexpressions,bothqualitativeandquantitativepropertiescanbeverifiedwithPLSMC.
Moreover,PLSMCisaneffectivemodelcheckingtooltotacklethestatespaceexplosionproblem.
Finally,safetyanditerativepropertiesofarailwayandhighwaycrossingguardrailcontrolsystemarecheckedwithPLSMC.
ExperimentalresultsshowthatthepresentedsymbolicmodelcheckerforPPTLextendsthevalidationfunctionalityoftheNuSMVsystemsuchthatstatesensitive,concurrentandperiodicpropertiescanbespecifiedandverifiedwithPPTL.
Keywords:symbolicmodelchecking;temporallogic;modelchecker;embeddedsystemverification基金项目:国家自然科学基金(61133001,61202038,61272117,61272118,61322202);国家重点基础研究发展计划(973)(2010CB328102)收稿时间:2013-05-20;修改时间:2013-09-09;定稿时间:2014-07-01逄涛等:一个命题投影时序逻辑符号模型检测器1969模型检测[1]是一种验证并发系统性质的重要形式化方法,它将被验证系统的行为建模为有限状态机,如Kripke结构[2]、状态迁移系统或者自动机;将系统期望的性质描述为时序逻辑公式.
然后,穷举搜索有限状态机以检查性质是否满足,并在不满足时提供反例.
相对于其他形式化方法,如定理证明[3]和等价性验证[4]等,模型检测具有自动化程度高、不需要用户干预、在验证失败后可以给出反例等优点.
近30年来,提出了很多智能和优秀的模型检测工具,如SPIN[5,6],NuSMV[7],NuSMV2[8],CHESS[9]和BLAST[10]等,用于通信协议、软硬件系统和嵌入式系统等的验证.
特别地,NuSMV是由CarnegieMellonUniversity和IstitutoperlaRicercaScientificaeTecholgica(IRST)联合开发的基于计算树逻辑(computationtreelogic,简称CTL)[11]和线性时序逻辑(lineartemporallogic,简称LTL)[12]的符号模型检测系统.
它非常适合于硬件电路和嵌入式系统的验证,可以有效地缓解SPIN和CHESS等显式状态模型检测工具可能出现的组合状态空间爆炸问题,并与BLAST等基于谓词抽象方法的模型检测系统互为补充,因此受到了学术界和工业界的广泛认可.
然而,上述模型检测工具的规范语言如CTL和LTL等的描述能力有限[13],不足以描述ω正则语言的性质,如"请求信号的振荡频率为4MHz(即,每250个时钟周期发生一次振荡)"、"在收到请求信号的第15个~第40个时钟周期内授权信号有效"等,使得一些时间敏感、并发性和周期性等实时相关的性质不能被描述和验证.
因此,扩展现有模型检测工具形式化规范语言的描述能力具有重要意义.
命题投影时序逻辑(propositionalprojectiontemporallogic,简称PPTL)[14,15]引入了projection等新的操作符,且描述能力等价于完全正则语言[16],它很适合被用作模型检测的规范语言.
性质"请求信号的振荡周期为250个时钟周期"和"在收到请求信号的第15个到第40个时钟周期内授权信号有效"可以方便地被描述为PPTL公式:len(250)*prjrequest和request→len(15);grant∧len(25);true.
文献[5]中提出了基于SPIN的命题投影时序逻辑模型检测方法,扩展了SPIN的功能,使得它能够支持PPTL公式的验证.
它将以Promela语言描述的系统模型和以Never-Claim结构描述的PPTL公式分别转化为Büchi自动机,并将两个自动机求积,通过判断积自动机接受字是否为空的方法验证系统模型是否满足期望的性质.
然而该工具基于显式状态空间描述,当被验证系统规模过大或者期望的性质较为复杂时,极易引发组合状态空间爆炸问题.
此外,该工具仅能处理以有限模型的PPTL公式描述的性质,无法验证无限模型的PPTL公式.
针对上述问题,文献[17]提出了PPTL的符号模型检测方法.
它使用规约有序二叉决策图(reducedorderedbinarydecisiondiagram,简称ROBDD)[18]符号化描述被验证系统模型,借助于ROBDD的压缩存储和有效地状态空间操作机制应对状态空间爆炸问题;使用PPTL公式描述系统期望的性质,借助于PPTL的完全正则表达能力扩展模型检测形式化规范的描述能力.
此外,该方法同时支持对于有限和无限模型PPTL公式的验证.
目前,已有基于CTL和LTL的符号模型检测工具,如NuSMV[7]和NuSMV2[8]等,但上述工具均不支持PPTL的符号模型检测方法.
本文基于NuSMV系统和PPTL符号模型检测方法的特点,提出了PPTL符号模型检测工具PLSMC的设计和实现过程.
该工具首先通过语言解析模块解析以SMV[19]语言符号化描述的系统模型M=(S,I,R,L)和以PPTL公式φ描述的系统期望性质,分别得到系统模型的语法树和PPTL性质公式的范式[14];其次,由编译模块对语法树执行扁平化、状态变量以及迁移关系编码等操作,得到符号化的系统模型;再次,依据NuSMV提供的符号化状态空间遍历机制和模型检测模块中实现的PPTL符号模型检测方法递归地计算状态结合S中满足的状态集合Sat();最后,将Sat()与初始状态集合I进行集合与操作,通过判断与操作结果是否为空集检测系统模型是否满足期望的性质,并在不满足时给出反例路径.
与其他模型检测工具相比,PPTL符号模型检测工具PLSMC的主要贡献如下:(1)该工具的性质规范语言PPTL具有完全正则表达能力,使得时间敏感性质、周期性质和并发性质等实时相关性质可以被方便地描述和验证,而其他工具的规范语言描述能力有限,无法完整地描述上述性质.
(2)该工具基于著名的符号模型检测工具NuSMV和PPTL符号模型检测方法实现,可以有效地应对基于显式状态空间描述的模型检测工具(如SPIN和CHESS等)中容易出现的组合状态空间爆炸问题.
(3)该工具可验证基于SPIN的PPTL模型检测工具无法验证的以无限模型PPTL公式描述的性质.
1970JournalofSoftware软件学报Vol.
26,No.
8,August2015本文第1节简要介绍命题投影时序逻辑的基本概念,包括语法和语义等.
第2节介绍命题投影时序逻辑符号模型检测方法的基本思想.
第3节给出PLSMC工具的设计和实现过程.
第4节通过对铁路公路交叉道口护栏控制系统的验证实例来展示PLSMC工具的正确性.
第5节通过若干实验结果来展示PLSMC工具的运行效率.
第6节是对本文的总结和对未来工作的展望.
1命题投影时序逻辑命题投影时序逻辑[14,15]是一种描述并发系统性质的有效形式化语言,它引入了新的投影时序操作符.
设Prop是一个可数原子命题集合,PPTL公式的语法定义如下:::=p|||1∨2|(1,.
.
.
,m)prj.
其中,p∈Prop,i(1≤i≤m)和为一般的PPTL公式;""(next)和"prj"(projection)为时序操作符.
如果一个PPTL公式包含时序操作符,则称为时序公式;否则,称为状态公式.
状态s定义为从Prop到集合B={true,false}的映射s:Prop→B.
用s[p]来表示命题p在s状态下的值,s[p]=true表示p在s状态下成立;反之,不成立.
区间σ=s0,s1,.
.
.
,s|σ|是一条有限或者无限状态序列.
对于有限区间,区间长度|σ|为状态数减1;对于无限区间,|σ|=ω,其中,状态s|σ|未定义.
另外,σ1σ2表示由区间σ1的结束状态与区间σ2的起始状态连接成一个新的区间.
σ(i.
.
.
j)表示σ的子区间si,.
.
.
,sj.
为定义投影操作符的语义,需要定义辅助操作符↓.
设区间σ=s0,s1,.
.
.
,r1,.
.
.
,rh(h≥1)是整数且0≤r1≤.
.
.
≤rh/|σ|.
其中,"/"定义为≤{ω,ω},表示≤中不包含ω=ω的情况.
σ在序列r1,.
.
.
,rh的投影为121lhtttrrsssσ↓=其中,t1,.
.
.
,tl是删除r1,.
.
.
,rh中的重复元素所得的严格递增序列子序列,例如,s0,s1,s2,s3↓(0,0,2,2,3)=s0,s2,s3.
解释I=(σ,k,j)是一个三元组,其中,σ表示一个区间,k为整数,j为整数或者ω,0≤k/j≤|σ|.
IB表示解释I=(σ,k,j)满足公式.
解释的归纳定义如下:IBp当且仅当s[p]=true;IB当且仅当IH;IB1∨2当且仅当IB1或IB2;IB当且仅当k0)个被满足.
(1;2)表示1和2被区间顺序满足.
定义1(范式).
设pProp为PPTL公式中出现的原子命题的集合,的范式为(e∧empty)∨(1mi=∨(i∧i′)),其中,e和i可以为true,或者形为1.
.
.
nrr∧∧的合取式,l=|p|,0≤m≤2l,0≤n≤l;rn属于p,且对于任意r∈p,r表示r或者r;i′是一个一般的PPTL公式.
如图2所示,范式由present部分和future部分组成.
present部分是一个状态公式,如e和i;future部分可以是empty或者是用""操作符修饰的一般PPTL公式,如i′.
其中,e∧empty表示present部分e在当前状态s0成立,且s0是满足公式e∧empty的区间的最后一个状态;i∧i′表示present部分i在区间σ的当前状态0s′成立,而future部分在子区间上12345sssss满足,且有σBi∧i′.
PPTL公式的范式刻画了满足该公式的状态集合的特征,已经证明,可以将任意PPTL公式等价地转化为其范式,转化算法的具体细节参见文献[20].
2PPTL符号模型检测算法模型检测将被验证系统行为建模为有限状态机M;将系统期望的性质描述为时序逻辑公式.
通过检查M是否满足来验证系统模型是否满足期望的性质.
由于系统模型大多基于显式状态空间描述,可验证系统的规模十分有限;在实际系统设计过程中,系统模型往往随系统并发组件的数目呈指数级增长.
因此,模型检测受制于组合状态空间爆炸问题.
此外,现有的模型检测方法的规范语言描述能力有限,使得周期性和并发性等实时相关性质无法被描述和验证.
针对上述问题,文献[17]中提出了命题投影时序逻辑的符号模型检测方法.
由于符号模型检测提供基于ROBDD的状态空间压缩存储和操作机制,加之PPTL的表达能力等价于完全正则语言[16],因此该算法可有效地应对组合状态空间爆炸问题,并且提高模型检测规范语言的描述能力.
在PPTL符号模型检测方法中,集合的操作均由基于ROBDD的布尔操作实现,其基本思想如下:(1)使用ROBDD符号化描述以Kripke结构M=(S,I,R,L)建模的待验证系统模型,用PPTL公式刻画系统期望的性质.
(2)将性质公式等价地转换成其范式NF,并根据范式语义从的最简单子公式开始,递归地求出模型M中满足的子公式的状态集合,并逐步扩展,最终得到满足的状态集合Sat().
(3)以状态集合S为全集对Sat()求补集,得到满足的状态集合Sat(),并判断Sat()和初始状态集合IS的交集Sat()∩I是否为空:如果为空,则系统模型M满足性质;否则不满足,且从Sat()∩I中的任意的状态出发都可以求出一条反例路径.
3PLSMC的设计与实现NuSMV[7]是基于CTL和LTL的符号模型检测系统,在NuSMV系统中,待验证系统行为模型通过SMV输123,.
.
.
,m1mi′e∧emptyi∧i′0s′1s′2s′3s′4s′5s′s0…Fig.
1Semanticsofformula(1,2,.
.
.
,m)prj图1公式(1,2,.
.
.
,m)prj的语义Fig.
2NormalformofPPTL图2PPTL的范式1972JournalofSoftware软件学报Vol.
26,No.
8,August2015入语言[19]描述,系统期望的性质采用经典的CTL或LTL公式来表达.
NuSMV通过内嵌的SMV输入语言解析模块解释系统的SMV模型,形成以ROBDD符号化描述的系统模型;并利用CTL或LTL解析模块求出性质公式所有的子公式.
然后,从性质公式的最基本的子公式开始,基于符号化系统模型递归求出满足性质公式的初始状态集合.
最后,对此状态集合求补集,获得不满足性质公式的初始状态集合.
若该集合为空,则系统模型满足期望的性质,输出true;否则,输出false并给出反例.
然而,NuSMV系统不支持对以PPTL公式描述的性质进行验证.
本节基于NuSMV和PPTL符号模型检测方法的特点,设计和实现了PPTL符号模型检测工具PLSMC.
3.
1PLSMC体系结构PLSMC工具的体系结构设计如图3所示.
该工具主要由6个松散耦合的模块构成:用户接口模块(userinterface)、解析模块(parser)、编译模块(compile)、性质公式存储模块(proposition)、模型检测模块(modelchecking)和CUDD模块.
其中,Parser模块内嵌将性质公式转化为良好形式(well-formed-formula)的Wff模块.
Fig.
3ArchitectureofPLSMC图3PLSMC体系结构用户接口模块支持用户以命令行和图形界面两种方式输入待验证系统的SMV语言模型和以PPTL公式描述的系统性质,输入文件可以使用任意文本编辑器进行编辑.
由于NuSMV系统不支持PPTL公式中常用的时序操作符,表1给出了PLSMC工具中扩展的PPTL时序操作符及其含义、优先级以及对应的ASCII码表示.
Table1TemporaloperatorsavailableinPLSMC表1PLSMC支持的时序操作符操作符含义优先级ASCII码例子Negation1!
!
Next2()()Sometimes2Always2[][]+Chop-Plus2++*Chop-Star2**∧And3&&1&&2∨Or3||1||2→Imply4→1→2Iff412;Chop5;1;2prjProjection5prj(1;2)prj用户接口(userinterface)解析器(parser)SMV语言解析器公式解析器(Wff)pptl2nf编译(compile)性质公式存储(Prop)PropDb模型检测(Mc)Mc_CheckPPtlSpecCUDD验证结果性质公式SMV模型逄涛等:一个命题投影时序逻辑符号模型检测器1973Parser模块基于SMV语言以及PPTL的词法和语法规则对用户输入的SMV系统模型和PPTL性质公式进行解析.
如果系统模型或者性质公式的词法或语法有错误,则将错误类型和位置返回给用户界面,提示用户进行修改;如果没有错误,则将系统模型翻译成语法树,并调用Wff模块将PPTL公式等价地转化为其范式,然后将范式及所有子公式存储在Prop模块中.
特别地,在NuSMV系统中,Wff模块负责将以CTL和LTL描述的性质公式转化为良好形式,PLSMC工具扩展了该模块的功能,集成了PPTL范式转化工具pptl2nf[5,16,20].
Compile模块从Parser模块获取系统模型的语法树,并依次对语法树执行扁平化(flattenhierarchy)、变量编码(encodevariables)以及模型构建(buildmodel)等操作,分别得到扁平化模型(flattenedmodel)、代数决策图(algebraicdecisiondiagram,简称ADD)模型和ROBDD模型.
然后,将ROBDD模型传递给Mc模块,作为PPTL符号模型检测过程的模型输入.
Prop模块定义了PropDb数据结构,用于存储Parser模块解析得到的性质公式范式及其子公式.
PLSMC系统运行时,该模块根据Mc模块的需要从PropDb中取回性质公式,对性质公式的类型进行判断,然后将结果返回给Mc模块.
经过扩展的Prop模块支持公式类型有Prop_ctl,Prop_ltl,Prop_psl以及Prop_pptl等.
Mc模块为PLSMC工具的核心模块.
该模块执行PPTL的符号模型检测过程.
它从Compile模块获得符号化的系统模型,从Prop模块中获得系统性质公式;然后,根据PropDb返回的公式类型调用相应的操作对性质公式进行验证,并将验证结果返回给用户界面显示.
如果性质不成立,则会输出反例提示.
该模块为用户查找和定位系统模型中的错误和缺陷提供必要的帮助.
CUDD模块提供高效的布尔函数操作.
该模块基于美国科罗拉多大学研发的CUDD软件包[21]实现Compile模块中符号化系统模型的构建、Mc模块中系统模型的遍历以及状态集上的集合操作等.
3.
2PLSMC实现依据如图3所示的体系结构设计图,PLSMC符号模型检测工具采用C/C++语言开发,基于Linux平台运行.
PLSMC工具的模型检测过程如图4所示,其中,阴影部分表示基于文献[17]中的PPTL符号模型检测方法扩展并实现的函数或操作,"a::b"表示框架设计图3中a模块所包含的b函数或b操作.
(1)将以SMV语言描述的待验证系统模型和系统期望的性质输入到PLSMC中.
(2)符号化描述待验证系统模型:1)Parser模块调用ReadModel函数检查系统的SMV模型是否满足词法和语法规则:若满足,则输出系统模型的语法树(syntaxtree);如果不满足,则将错误信息返回用户界面,提示用户进行修改;2)Compile模块调用FlattenHierarchy函数去除语法树中模块间的层级关系,输出扁平化系统模型;3)Compile模块调用EncodeVariables函数对扁平化系统模型中的状态变量进行编码,输出以ADD符号化描述的系统模型;4)Compile模块调用BuildModel函数将ADD系统模型中的初始状态和迁移关系采用ROBDD描述,输出以ROBDD符号化描述的系统模型.
(3)计算期望性质公式的良好形式:1)Parser模块判断性质公式的类型:如果不是PPTL公式,则交由NuSMV系统按照CTL或LTL的符号模型检测流程进行处理;如果是PPTL公式,则交给Wff模块中集成的pptl2nf工具处理;2)pptl2nf工具计算出PPTL性质公式的范式NF及所有子公式,并存储在Prop模块的PropDb中.
(4)判断系统模型是否满足期望的性质:1)Mc模块调用CheckPPtlSpec函数从PropDb数据结构中提取性质公式的范式NF及其子公式,由Prop模块判断公式类型,并将公式类型(设为Prop_pptl)传递给PropDb_verify_all_type函数;2)PropDb_verify_all_type函数根据参数类型(设为Prop_pptl),依次调用Mc模块的eval_pptl_spec和eval_pptl_spec_recur函数,从NF的最简单子公式开始,逐步扩展求得ROBDD系统模型中满足的状态集合Sat();3)对集合Sat()求补集,获得满足的状态集合Sat().
若该集合与初始状态集合I的交集1974JournalofSoftware软件学报Vol.
26,No.
8,August2015Sat()∩I为空,则系统模型满足期望的性质,输出true;否则,输出false并给出反例路径.
Fig.
4FlowchartofPLSMC图4PLSMC流程图注意,如图4所示的流程图中核心部分为圆角矩形虚线框中的eval_pptl_spec和eval_pptl_spec_recur函数.
这两个函数实现了文献[17]中提出的PPTL符号模型检测方法,使得PLSMC工具支持对以PPTL公式描述的期望性质进行验证.
图中所示的符号化系统模型的构建、模型的遍历以及状态集上的集合操作均由CUDD模块提供的ROBDD操作函数实现.
此外,由于步骤(2)和步骤(3)之间不存在数据共享,因此这两个步骤可以并行执行,从而加快工具的运行效率.
4验证实例4.
1铁路公路交叉道口护栏控制系统在铁路与公路的平交道口上,为防止铁路段车辆与公路段车辆以及行人同时进入道口发生冲撞危险,一般通过升降护拦控制铁路和公路段的交通流量.
如图5所示,基于可编程控制器(programmablelogiccontroller,简称PLC)的护栏控制系统(guardrailcontrolsystem,简称GCS),由PLC控制器、双侧护拦、护栏电机、传感器、警报器和红绿灯等部件组成.
下面以火车自西向东方向运行通过交叉道口为例,解释GCS系统的运行过程:(1)系统处于空闲状态时,护拦打开,火车运行在道口之外,公路段绿灯和铁路段红灯处于点亮状态.
公路段的汽车和行人允许通过道口,铁路段禁止通行.
Parser::ReadModel否错误信息错误信息语法树Compile::FlattenHierarchy扁平化模型Compile::EncodeVariablesADD模型Compile::BuildModelROBDD模型SMV模型正确PLSMC是PPTLNuSMVMc::eval_pptl_specMc::eval_pptl_recurWff::pptl2nf的范式NF正确性质公式Mc::CheckPptlSpecProp::PropDb_verify_all_type(Prop_pptl)MB反例否是是否是否逄涛等:一个命题投影时序逻辑符号模型检测器1975(2)火车沿自西向东方向运行到达预知传感器1(灰色矩形)时,警报器蜂鸣提示道口中汽车和行人尽快离开道口,公路段绿灯和铁路段红灯此时仍处于点亮状态.
(3)警报器蜂鸣持续3分钟后,公路段和铁路段黄灯点亮,PLC控制器通过护栏电机控制护拦下降.
(4)公路段和铁路段黄灯点亮持续2分钟后,护拦关闭,公路段红灯和铁路段绿灯点亮,公路段禁止通行,火车花费1~3分钟通过道口.
(5)火车经过道口达到东侧预知传感器2(灰色矩形)时,公路段和铁路段黄灯点亮,警报器关闭,PLC控制器通过护栏电机控制护拦上升.
(6)公路段和铁路段黄灯点亮持续2分钟后,公路段绿灯和铁路段红灯点亮,护拦处于打开状态,铁路段禁止通行,公路段的汽车和行人允许进入道口,系统转到空闲状态.
(7)如果自东向西和自西向东方向均没有火车通过道口,那么系统将一直在空闲状态驻留.
Fig.
5Railwayandhighwaycrossingguardrailcontrolsystem图5铁路、公路交叉道口护栏控制系统铁路公路交叉道口的防护对提高铁路、公路的通过能力和保证汽车及行人安全具有重要的意义.
本节将对上述GCS系统的实时安全性质和迭代性质进行分析和描述,并采用PPTL符号模型检测工具PLSMC对其进行验证;同时,检验该工具的设计和实现过程的正确性.
4.
2护栏控制系统建模为了使用PLSMC工具对GCS系统进行验证,需要使用SMV语言对系统行为进行建模.
SMV语言的具体细节参见文献[19].
下面分析并定义GCS系统的状态变量.
火车到达西侧预知传感器1时警报器蜂鸣,火车离开道口到达东侧预知传感器2时警报器关闭.
因此,定义布尔类型的变量alert表示火车的到达与离开:alert:boolean.
例如,alert=TRUE,表示火车到达交叉道口西侧预知传感器1时,警报器蜂鸣;alert=FALSE,表示火车离开交叉道口到达东侧预知传感器2时,警报器关闭.
公路和铁路段各有一组红、绿、黄三色交通灯,在车辆和行人通过道口时提供必要的提示.
因此定义两个枚举类型的变量railway_light和highway_light表示各个交通灯当前所处的状态:railway_light:{red,green,yellow};highway_light:{red,green,yellow};例如,highway_light=yellow表示公路段的黄灯处于点亮状态.
此外,依据GCS系统的功能描述,公路段红灯和铁护栏铁路公路PLC控制器传感器1传感器2传感器2铁路红灯公路绿灯公路黄灯铁路黄灯公路红灯铁路绿灯公路黄灯铁路黄红灯公路绿灯铁路红灯西东传感器1交通灯…1976JournalofSoftware软件学报Vol.
26,No.
8,August2015路段绿灯、公路段绿灯和铁路段红灯以及公路段黄灯和铁路段黄灯点亮后的持续时间相同,因此定义枚举型变量light_duration表示交通灯当前状态持续的时间:light_duration:{one,two,zero,stay}.
例如,railway_light=yellow&higway_light=yellow&light_duration=two表示公路段和铁路段的黄灯均持续点亮了2分钟.
注意:由于公路段绿灯和铁路段红灯在系统空闲时处于恒亮状态,只有当控制系统进入工作状态时才需要记录公路段绿灯和铁路段红灯点亮的持续时间,因此,定义stay表示系统空闲时公路段绿灯和铁路段红灯恒亮;定义zero表示控制系统进入工作状态,并准备记录当前处于点亮状态的交通灯的持续时间.
双侧护栏在护栏电机的控制下有打开、关闭、上升和下降4个状态,因此定义枚举型变量guardrail_status表示护栏当前所处的状态:guardrail_status:{open,closed,lowering,raising}.
例如,guardrail=lowering表示护栏处在下降状态.
依据上述状态变量的定义,GCS系统的初始状态或空闲状态可以用init关键字定义如下:init(alert):=FALSE;init(railway_light):=red;init(highway_light):=green;init(light_duration):=stay;init(guardrail_status):=open.
表示系统处于空闲状态时,火车未进入交叉道口alert=FALSE,护栏处于打开状态guardrail_status=open,公路段绿灯和铁路段红灯处于恒亮状态light_duration=stay.
通常情况下,如果没有特别说明,以状态迁移结构描述的系统模型中,所有状态迁移均在单位系统时间内完成.
设计人员可以根据验证需求选择合适的时间粒度作为系统时间标准.
在这里,规定GCS系统的标准时间为1分钟,那么状态迁移关系可由当前状态的状态变量取值和下一状态状态变量取值共同描述.
例如,next(guardrail_status):=case(alert&railway_light=red&highway_light=green&light_duration=two&guardrail_status=open)|…:lowering;(alert&railway_light=green&highway_light=red&light_duration=zero&guardrail_status=closed)|…:raising;(alert&railway_light=yellow&highway_light=yellow&light_duration=one&guardrail_status=lowering)|…:closed;(!
alert&railway_light=red&highway_light=green&light_duration=stay&guardrail_status=open)|…:open;TRUE:open;esac;其含义是:(1)如果当前状态警报器蜂鸣,铁路段红灯和公路段绿灯持续点亮2分钟且护栏打开时,下一状态护栏将处于下降状态;(2)如果当前状态警报器蜂鸣,铁路段绿灯和公路段红灯刚点亮且护栏处在关闭状态时,下一状态护栏将处于上升状态;(3)如果当前状态警报器蜂鸣,铁路段和公路段黄灯持续点亮1分钟且护栏正在下降时,下一状态护栏处于关闭状态;(4)如果当前状态警报器关闭,铁路段红灯和公路段绿灯恒亮且护栏打开时,下一状态护栏仍将处于打开状态.
注意:在上述状态变量guardrail_status的状态迁移描述中,"|…"表示存在其他条件使得护栏下一状态处于打开、关闭、上升和下降这4个状态.
限于篇幅,在此不再详述.
类似地,GCS系统行为模型中的状态变量的迁移关系,如next(alert),next(railway_light),next(highway_light)和next(light_duration)等均可用状态变量alert,railway_light,highway_hight,light_duration和guardrail_status的取值变化及SMV语言提供的关键字如next,case和操作符&(逻辑与)、操作符|(逻辑或)等来描述.
逄涛等:一个命题投影时序逻辑符号模型检测器19774.
3GCS系统验证GCS系统的目的是保证火车进入道口前护栏已经关闭,行人和汽车离开道口,公路段红灯点亮禁止通行,铁路段绿灯点亮允许通行,而且在火车彻底离开道口前护栏不会打开.
使得公路方向的汽车或行人和来自铁路方向的火车不会因为同时进入道口而发生冲撞危险,同时又不会因为护栏关闭时间过长而影响公路方向的交通流量.
该系统的安全性可以描述为:(1)火车进入交叉道口前护栏已处于关闭状态,公路方向红灯和铁路方向绿灯点亮.
(2)护栏关闭后最多5分钟就会打开.
此外,由于没有火车通过道口时GCS系统可以在空闲状态长时间驻留,该系统的迭代性质可以描述为:(3)若当前状态系统处于空闲状态,那么将来状态GCS系统可转入工作状态,也可在空闲状态继续驻留.
从以上分析可以看出,GCS系统的安全性和迭代性分别为实时性质和循环性质,使用经典的CTL和LTL无法完整地描述.
PPTL是基于区间的时序逻辑,很适合描述时间敏感和周期性等实时性质;同时,PPTL中的*(chop-star)操作符可以方便地描述迭代性质.
因此,GCS系统的安全性和迭代性可以描述为以下PPTL公式:(1)(alert→(len(5);(guardrail_status=closed∧railway_light=green∧highway_light=red))∧empty;TRUE)).