2015, Vol. 26
2. 综合业务网理论与关键技术国家重点实验室(西安电子科技大学),陕西 西安 710071
2. State Key Laboratory of Integrated Services Networks (Xidian University), Xi'an 710071, China
模型检测[1]是一种验证并发系统性质的重要形式化方法,它将被验证系统的行为建模为有限状态机,如Kripke结构[2]、状态迁移系统或者自动机;将系统期望的性质描述为时序逻辑公式.然后,穷举搜索有限状态机以检查性质是否满足,并在不满足时提供反例.相对于其他形式化方法,如定理证明[3]和等价性验证[4]等,模型检测具有自动化程度高、不需要用户干预、在验证失败后可以给出反例等优点.近30年来,提出了很多智能和优秀的模型检测工具,如SPIN[5,6],NuSMV[7],NuSMV2[8],CHESS[9]和BLAST[10]等,用于通信协议、软硬件系统和嵌入式系统等的验证.特别地,NuSMV是由Carnegie Mellon University和Istituto per la Ricerca Scientifica e Techolgica(IRST)联合开发的基于计算树逻辑(computation tree logic,简称CTL)[11]和线性时序逻辑(linear temporal logic,简称LTL)[12]的符号模型检测系统.它非常适合于硬件电路和嵌入式系统的验证,可以有效地缓解SPIN和CHESS等显式状态模型检测工具可能出现的组合状态空间爆炸问题,并与BLAST等基于谓词抽象方法的模型检测系统互为补充,因此受到了学术界和工业界的广泛认可.然而,上述模型检测工具的规范语言如CTL和LTL等的描述能力有限[13],不足以描述w正则语言的性质,如“请求信号的振荡频率为4MHz(即,每250个时钟周期发生一次振荡)”、“在收到请求信号的第15个~第40个时钟周期内授权信号有效”等,使得一些时间敏感、并发性和周期性等实时相关的性质不能被描述和验证.因此,扩展现有模型检测工具形式化规范语言的描述能力具有重要意义.
命题投影时序逻辑(propositional projection temporal logic,简称PPTL)[14,15]引入了projection等新的操作符,且描述能力等价于完全正则语言[16],它很适合被用作模型检测的规范语言.性质“请求信号的振荡周期为250个时钟周期”和“在收到请求信号的第15个到第40个时钟周期内授权信号有效”可以方便地被描述为PPTL公式:
len(250)prj□request和request→len(15);◇grant⊦len(25);true.
文献[5]中提出了基于SPIN的命题投影时序逻辑模型检测方法,扩展了SPIN的功能,使得它能够支持PPTL公式的验证.它将以Promela语言描述的系统模型和以Never-Claim结构描述的PPTL公式分别转化为Büchi自动机,并将两个自动机求积,通过判断积自动机接受字是否为空的方法验证系统模型是否满足期望的性质.然而该工具基于显式状态空间描述,当被验证系统规模过大或者期望的性质较为复杂时,极易引发组合状态空间爆炸问题.此外,该工具仅能处理以有限模型的PPTL公式描述的性质,无法验证无限模型的PPTL公式.
针对上述问题,文献[17]提出了PPTL的符号模型检测方法.它使用规约有序二叉决策图(reduced ordered binary decision diagram,简称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公式描述的性质.
本文第1节简要介绍命题投影时序逻辑的基本概念,包括语法和语义等.第2节介绍命题投影时序逻辑符号模型检测方法的基本思想.第3节给出PLSMC工具的设计和实现过程.第4节通过对铁路公路交叉道口护栏控制系统的验证实例来展示PLSMC工具的正确性.第5节通过若干实验结果来展示PLSMC工具的运行效率.第6节是对本文的总结和对未来工作的展望.
1 命题投影时序逻辑命题投影时序逻辑[14,15]是一种描述并发系统性质的有效形式化语言,它引入了新的投影时序操作符.设Prop是一个可数原子命题集合,PPTL公式的语法定义如下:
φ::=p|○φ|¬φ|φ1⊥φ2|(φ1,...,φm) prj j.
其中,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;对于无限区间,|σ|=ω,其中,状态σ|σ|未定义.另外,σ1●σ2表示由区间σ1的结束状态与区间σ2的起始状态连接成一个新的区间. σ(i...j)表示σ的子区间〈si,...,sj〉.
为定义投影操作符的语义,需要定义辅助操作符↓.设区间σ=〈s0,s1,...〉,r1,...,rh(h≥1)是整数且0≤r1≤...≤rh≦ |σ|.其中,“ ”定义为≤-{ω,ω},表示≤中不包含ω=ω的情况.σ在序列r1,...,rh的投影为
σ↓(r1rh=〈st1,st2,...,stl〉)
其中,t1,...,tl是删除r1,...,rh中的重复元素所得的严格递增序列子序列,例如,〈s0,s1,s2,s3〉↓(0,0,2,2,3)=〈s0,s2,s3〉.
解释I=(σ,k,j)是一个三元组,其中,σ表示一个区间,k为整数,j为整数或者ω,0≤k j≤|σ|.I|=φ表示解释I=(σ,k,j)满足公式φ.解释的归纳定义如下:
· I|=p当且仅当s[p]=true;
· I|=¬φ当且仅当I|≠φ;
· I|=φ1⊥φ2当且仅当I|=φ1或I|=φ2;
· I|=○φ当且仅当k<j且(σ,k+1,j)|=φ;
· I|=(φ1,...,φm) prj φ,如果存在整数序列k=r0≤r1≤...≤rm≤j,使得(σ,r0,r1)|=φ1,(σ,rl-1,rl)|=φl(1≤l≤m),并且对于以下2种情况有(σ',0,|σ'|)|=φ:
(1) rm<j并且σ'=σ↓(r0,...,rm)●,σ(rm+1…j)或者
(2) rm=j并且有σ'=σ↓(r0,...,rh),其中,0≤h≤m.
如果(σ,0,|σ|)|=φ,那么公式φ在区间上σ是可满足的,记作σ|=φ;如果存在σ使得σ|=φ,则公式φ是可满足的;如果对于任意的σ,σ|=φ,则公式φ是有效的.常用的派生公式为
empty≡¬○true,more≡¬empty,skip≡len(1),◇φ≡true;φ,□φ≡¬◇¬φ
len(n)≡○nempty,○0φ≡φ,○nφ≡○(○n-1φ),φ1;φ2≡(φ1,φ2) prj empty.
直观来讲,上述PPTL公式在状态区间上的解释如下:
· ○φ表示φ在区间的下一状态成立.
· (φ1,...,φm) prj φ用两个不同的时间粒度刻画进程,如图1所示:细粒度的是由φ1,...,φm顺序复合而成的局部序列;粗粒度的是并行执行φ的全局序列.即,φ与φ1,...,φm在一个区间上并行执行,φ的执行区间由φ1,...,φm各自执行区间的端点组成.
|
Fig.1 Semantics of formula (φ1,φ2,…φm)prj φ 图 1 >公式(φ1,φ2,…φm)prj φ的语义 |
· empty表示当前区间长度为0.
· ◇φ表示φ将在区间将来某个状态被满足.
· □φ表示φ将在区间将来所有状态被满足.
· len(n)表示区间长度为n.
· ○nφ表示φ将在区间将来第n(n>0)个被满足.
· (φ1;φ2)表示φ1和φ2被区间顺序满足.
定义1(范式). 设φp⊆Prop为PPTL公式φ中出现的原子命题的集合,φ的范式为
(φe⊦empty)⊥(⊥i=1m(φi⊦○φi')),
其中,φe和φi可以为true,或者形为
如图2所示,范式由present部分和future部分组成.present部分是一个状态公式,如φe和φi;future部分可以是empty或者是用“○”操作符修饰的一般PPTL公式,如○φi'.其中,φe⊦empty表示present部分φe在当前状态s0成立,且s0是满足公式φe⊦empty的区间的最后一个状态;φi⊦○φi'表示present部分φi在区间σ的当前状态s0'成立,而future部分在子区间上〈
|
Fig.2 Normal form of PPTL 图 2 PPTL的范式 |
PPTL公式的范式刻画了满足该公式的状态集合的特征,已经证明,可以将任意PPTL公式等价地转化为其范式,转化算法的具体细节参见文献[20].
2 PPTL 符号模型检测算法模型检测将被验证系统行为建模为有限状态机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(¬φ)和初始状态集合I⊆S的交集Sat(¬φ)∩I是否为空:如果为空,则系统模型M满足性质φ;否则不满足,且从Sat(¬φ)∩I中的任意的状态出发都可以求出一条反例路径.
3 PLSMC 的设计与实现NuSMV[7]是基于CTL和LTL的符号模型检测系统,在NuSMV系统中,待验证系统行为模型通过SMV输入语言[19]描述,系统期望的性质采用经典的CTL或LTL公式来表达.NuSMV通过内嵌的SMV输入语言解析模块解释系统的SMV模型,形成以ROBDD符号化描述的系统模型;并利用CTL或LTL解析模块求出性质公式所有的子公式.然后,从性质公式的最基本的子公式开始,基于符号化系统模型递归求出满足性质公式的初始状态集合.最后,对此状态集合求补集,获得不满足性质公式的初始状态集合.若该集合为空,则系统模型满足期望的性质,输出true;否则,输出false并给出反例.然而,NuSMV系统不支持对以PPTL公式描述的性质进行验证.本节基于NuSMV和PPTL符号模型检测方法的特点,设计和实现了PPTL符号模型检测工具PLSMC.
3.1 PLSMC 体系结构PLSMC工具的体系结构设计如图3所示.该工具主要由6个松散耦合的模块构成:用户接口模块(user interface)、解析模块(parser)、编译模块(compile)、性质公式存储模块(proposition)、模型检测模块(model checking)和CUDD模块.其中,Parser模块内嵌将性质公式转化为良好形式(well-formed-formula)的Wff模块.
|
Fig.3 Architecture of PLSMC 图 3 PLSMC体系结构 |
用户接口模块支持用户以命令行和图形界面两种方式输入待验证系统的SMV语言模型和以PPTL公式描述的系统性质,输入文件可以使用任意文本编辑器进行编辑.由于NuSMV系统不支持PPTL公式中常用的时序操作符,表1给出了PLSMC工具中扩展的PPTL时序操作符及其含义、优先级以及对应的ASCII码表示.
|
Table 1 Temporal operators available in PLSMC 表 1 PLSMC支持的时序操作符 |
Parser模块基于SMV语言以及PPTL的词法和语法规则对用户输入的SMV系统模型和PPTL性质公式进行解析.如果系统模型或者性质公式的词法或语法有错误,则将错误类型和位置返回给用户界面,提示用户进行修改;如果没有错误,则将系统模型翻译成语法树,并调用Wff模块将PPTL公式等价地转化为其范式,然后将范式及所有子公式存储在Prop模块中. 特别地,在NuSMV系统中,Wff模块负责将以CTL和LTL描述的性质公式转化为良好形式,PLSMC工具扩展了该模块的功能,集成了PPTL范式转化工具pptl2nf[5,16,20].
Compile模块从Parser模块获取系统模型的语法树,并依次对语法树执行扁平化(flatten hierarchy)、变量编码(encode variables)以及模型构建(build model)等操作,分别得到扁平化模型(flattened model)、代数决策图(algebraic decision diagram,简称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.2 PLSMC 实现依据如图3所示的体系结构设计图,PLSMC符号模型检测工具采用C/C++语言开发,基于Linux平台运行. PLSMC工具的模型检测过程如图4所示,其中,阴影部分表示基于文献[17]中的PPTL符号模型检测方法扩展并实现的函数或操作,“a::b”表示框架设计图3中a模块所包含的b函数或b操作.
|
Fig.4 Flowchart of PLSMC 图 4 PLSMC流程图 |
(1) 将以SMV语言描述的待验证系统模型和系统期望的性质输入到PLSMC中.
(2) 符号化描述待验证系统模型:
1) Parser模块调用ReadModel函数检查系统的SMV模型是否满足词法和语法规则:若满足,则输出系统模型的语法树(syntax tree);如果不满足,则将错误信息返回用户界面,提示用户进行修改;
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的交集Sat(¬φ)∩I为空,则系统模型满足期望的性质,输出true;否则,输出false并给出反例路径.
注意,如图4所示的流程图中核心部分为圆角矩形虚线框中的eval_pptl_spec和eval_pptl_spec_recur函数.这两个函数实现了文献[17]中提出的PPTL符号模型检测方法,使得PLSMC工具支持对以PPTL公式描述的期望性质进行验证.图中所示的符号化系统模型的构建、模型的遍历以及状态集上的集合操作均由CUDD模块提供的ROBDD操作函数实现.此外,由于步骤(2)和步骤(3)之间不存在数据共享,因此这两个步骤可以并行执行,从而加快工具的运行效率.
4 验证实例 4.1 铁路公路交叉道口护栏控制系统在铁路与公路的平交道口上,为防止铁路段车辆与公路段车辆以及行人同时进入道口发生冲撞危险,一般通过升降护拦控制铁路和公路段的交通流量.如图5所示,基于可编程控制器(programmable logic controller,简称PLC)的护栏控制系统(guardrail control system,简称GCS),由PLC控制器、双侧护拦、护栏电机、传感器、警报器和红绿灯等部件组成.下面以火车自西向东方向运行通过交叉道口为例,解释GCS系统的运行过程:
|
Fig.5 Railway and highway crossing guardrail control system 图 5 铁路、公路交叉道口护栏控制系统 |
(1) 系统处于空闲状态时,护拦打开,火车运行在道口之外,公路段绿灯和铁路段红灯处于点亮状态.公路段的汽车和行人允许通过道口,铁路段禁止通行.
(2) 火车沿自西向东方向运行到达预知传感器1(灰色矩形)时,警报器蜂鸣提示道口中汽车和行人尽快离开道口,公路段绿灯和铁路段红灯此时仍处于点亮状态.
(3) 警报器蜂鸣持续3分钟后,公路段和铁路段黄灯点亮,PLC控制器通过护栏电机控制护拦下降.
(4) 公路段和铁路段黄灯点亮持续2分钟后,护拦关闭,公路段红灯和铁路段绿灯点亮,公路段禁止通行,火车花费1~3分钟通过道口.
(5) 火车经过道口达到东侧预知传感器2(灰色矩形)时,公路段和铁路段黄灯点亮,警报器关闭,PLC控制器通过护栏电机控制护拦上升.
(6) 公路段和铁路段黄灯点亮持续2分钟后,公路段绿灯和铁路段红灯点亮,护拦处于打开状态,铁路段禁止通行,公路段的汽车和行人允许进入道口,系统转到空闲状态.
(7) 如果自东向西和自西向东方向均没有火车通过道口,那么系统将一直在空闲状态驻留.
铁路公路交叉道口的防护对提高铁路、公路的通过能力和保证汽车及行人安全具有重要的意义.本节将对上述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系统的功能描述,公路段红灯和铁路段绿灯、公路段绿灯和铁路段红灯以及公路段黄灯和铁路段黄灯点亮后的持续时间相同,因此定义枚举型变量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和操作符&(逻辑与)、操作符|(逻辑或)等来描述.
4.3 GCS 系统验证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)).
任意时刻,火车到达传感器1,警报器蜂鸣5分钟后,护栏关闭,公路段红灯和铁路段绿灯点亮.
(2) □(alert→(◇(□(guardrail_status=closed⊦(len(1)⊥len(2)⊥len(3)⊥len(4)⊥len(5))));TRUE)).
任意时刻,警报器蜂鸣后护栏将会关闭,关闭持续时间不超过5分钟.
(3) (light_duration=stay);○((light_duration=zero)⊥(light_duration=stay)*).
当前状态系统空闲,下一状态系统将转入工作状态或者在空闲状态发生有限多次自身转移(self-transition).
这里仅通过性质(1)和性质(3)来验证GCS系统的安全性、迭代性以及PLSMC工具的正确性,其他性质的验证过程类似.如图6(a)上半部分所示,将系统的SMV模型和以SPEC关键字修饰的PPTL公式输入到PLSMC工具后,系统提示没有错误,性质(1)成立.因此,GCS系统满足“火车进入交叉道口前护栏已处于关闭状态,公路方向红灯和铁路方向绿灯点亮”这一安全性质.
|
Fig.6 Verification result 图 6 验证结果 |
如果将性质(1)改为
□(alert→(len(2);(guardrail_status=open⊦railway_light=yellow⊦highway_light=yellow))⊦empty;TRUE)),
即,在任意时刻火车到达预知传感器1,警报器蜂鸣后2分钟护栏打开,公路段和铁路段黄灯同时点亮.系统提示有错误,并生成相应的反例路径.如图6(b)给出的反例路径所示,在state:1.2时,火车到达预知传感器1,警报器蜂鸣alert=TRUE;2分钟后,即,经过两个状态迁移到达state:1.4时,铁路段红灯与公路段绿灯点亮且持续了2分钟,护栏打开,而不是性质规范描述的护栏打开,公路段和铁路段黄灯点亮:
guardrail_status=open⊦railway_light=yellow⊦highway_light=yellow.
类似地,如图6(a)下半部分所示,性质(3)成立.因此,GCS系统满足性质“若当前状态系统处于空闲状态,那么将来状态GCS系统可以转入工作状态,也可在空闲状态继续驻留”.
PLSMC工具提供的验证结果显示,GCS系统满足其安全性质和迭代性质,间接说明了该工具设计和实现过程的正确性.此外,在对其他系统进行功能验证时,可借助PLSMC工具提供的反例路径,对系统功能进行调整和修改.
5 实验结果在Fedora GNU/Linux 7.0(内核版本2.6.21)平台+HP Z800工作站(Intel Xeon 2.67GHZ 2.66GHZ/12G)上,通过卡内基梅隆大学及Fondazione Bruno Kessle组织提供的若干模型检测典型案例对PLSMC工具的性能进行了一系列实验评估,并与NuSMV 2.5.4版本进行了比较.实验主要关注以下两个方面的问题:
(1) 通过对可同时用CTL/LTL和PPTL公式描述的性质进行验证,比较NuSMV和PLSMC工具的效率;
(2) 通过对只能用PPTL公式描述的性质进行验证,展示PLSMC的效率和可处理问题的规模.
如果没有特别说明,实验结果中的运行时间开销均为10次模型检测过程中系统时间(system time)与用户时间(user time)之和的平均值;空间开销用可达状态数与公式长度之积来评估;“-”表示工具运行失败或者超时,“-coi”表示使用影响椎规约(cone of influence reduction)参数后系统运行的时间开销.
5.1 Gigamax 缓存一致性协议检测实验结果Gigamax是一种分布式共享内存多处理器体系结构.在Gigamax体系结构中,处理器被划分为多个cluster,每个cluster通过本地总线和总线探测机制维护其内部处理器缓存的一致性;同时,cluster通过UIC接口及全局总线与其他cluster相连,UIC接口在cluster之间充当总线探测器与总线主设备的作用,从而使所有cluster内部缓存保持一致.文献[19]中给出了Gigamax缓存一致性协议的SMV语言模型,其对应的NuSMV和PLSMC验证结果见表2.
|
|
Table 2 Model checking results for Gigamax cache coherence protocol 表 2 Gigamax缓存一致性协议模型检测结果 |
在表2中,CTL公式AGEF(p0.readable)表示从初始状态出发的所有路径中均存在一个状态使得处理器p0可以读取缓存内容;公式AG!(p0.writable&p1.writable&p2.writable)表示在任何状态下均不允许处理器p0,p1和p2同时执行写缓存操作.上述公式在NuSMV工具验证的时间开销分别为0.032s/0.032s和0.023s/0.027s.由于PLSMC工具是对NuSMV系统的扩展,因此二者在验证CTL性质时的时间消耗一致.特别地,上述性质也可用PPTL公式[]〈〉(p0.readable)和[](!(p0.writable&p1.writable&p2.writable))来描述,其对应的时间开销分别为0.098s/0.101s和0.038s/0.039s.
5.2 交替位协议检测实验结果交替位协议[22]是一种工作在数据链路层的网络通信协议,主要用于在发送者与接受者之间重传丢失或者损坏的数据包.如图7所示,它由Sender,Receiver,S2R和R2S这4个主要构件组成.Sender从用户处取得数据并通过发送通道S2R将消息./data(b,d)发送给Receiver,其中,b∈{0,1}表示发送消息的序列号,d表示任意宽度的数据; Receiver从S2R获得消息传送给用户,并通过反馈通道R2S返回确认消息ack(b).Sender会不断重发同一序列号的消息,直到从Receiver处获得该序列号的确认消息,然后将序列号b的值翻转;Receiver会不断重发同一序列号的确认消息,直到从S2R获得包含其他序列号的消息.交替位协议的验证结果见表3,其中,CTL公式AGAF (se nder.state=get)以及PPTL公式[]〈〉(sender.state=get)均表示沿着交替位协议模型的所有路径出发均可到达某个状态,使得在该状态下Sender从用户处取得数据sender.state=get.PLSMC和NuSMV在验证上述CTL性质时的时间消耗均为0.042s/0.018s;在验证PPTL性质时NuSMV运行失败,而PLSMC的时间开销为0.043s/0.018s.特别地,PPTL公式:
|
Fig.7 Alternating bit protocol 图 7 交替位协议 |
|
|
Table 3 Model checking results for alternating bit protocol 表 3 交替位协议模型检测结果 |
(sender.state=get)&&()(sender.state=send)→(〈〉(sender.state=wait_for_ack)+;(sender.state=get))
表示Sender获得用户数据sender.state=get并发送sender.state=send后,将转入等待响应状态sender.state=wait_ for_ack,并且需要在该状态逗留有限多个时钟周期(sender.state=wait_for_ack)+,直到收到Receiver的确认消息后才能重新进入接收用户数据状态,开始下一次消息的发送.由于上述性质为完全正则性质,使用经典的CTL或者LTL公式均无法完整地描述,因此NuSMV运行失败,而PLSMC的运行时间开销为0.056s/0.028s.
5.3 PCI 总线检测实验结果PCI是一种重要的总线设计规范,它规定了局部总线的物理结构、电气特性、总线时序和通信协议等,支持网卡、声卡、调制解调器和磁盘控制器等多种外部设备与处理器的连接.文献[22]给出了如图8所示的PCI总线仲裁机构模型,它包含2层仲裁机制并支持最多6个设备同时提起总线操作请求,由3个2输入/1输出和1个3输入/1输出的总线仲裁器件构成.每个仲裁器可以根据需要选择仲裁策略为固定优先级(fixed priority)或者是循环优先级(round robin).PCI总线协议的验证结果见表4.
|
Fig.8 PCI bus protocol 图 8 PCI总线协议 |
|
|
Table 4 Model checking results for PCI bus protocol 表 4 PCI总线协议模型检测结果 |
在表4中,CTL公式AG(isa_bridge.req→A(isa_bridge.reqUarb.grant=0)表示设备isa_bridge发出总线请求isa_bridge.req后,请求信号将一直保持高电平,直到仲裁机构返回对于该请求的总线使用授权信号arb.grant=0.类似地,PPTL公式[](isa_bridge.req→(isa_bridge.req )*;arb.grant=0)表示若isa_bridge.req信号为高电平,那么该信号将保持有限多个时钟周期(isa_bridge.req)*直到仲裁机构返回总线使用授权信号.NuSMV和PLSMC在验证CTL公式时的运行时间基本一致;在验证PPTL公式时前者运行失败,后者的时间时效开销在使用-coi参数后明显优于前者.特别地,PPTL公式:
〈〉(all_req→(arb.grant=0;arb.grant=1;arb.grant=2;arb.grant=3;arb.grant=4;arb.grant=5) prj arb.out)
表示若当前时钟周期所有设备均提出总线使用请求,则
all_req≡isa_bridge.req&&scsi_ctrl.req&&vga_ctrl.req&&slot0.req&&processors.req&&slot1.req.
在未来的时钟周期内,图8中的6个设备将会依次获得总线占用权(设所有仲裁构件均采用固定优先级仲裁策略),且授权过程与仲裁机构的授权输出:
arb.out≡arb.grant=0||arb.grant=1||arb.grant=2||arb.grant=3||arb.grant=4||arb.grant=5||arb.grant=idle
是并行执行的.由于上述性质为并行性质,因此仅能使用PPTL新引入的投影时序操作符prj描述,PLSMC在验证该性质时所花费的时间为6.755s/1.094s.
通过对上述案例的实验结果对比分析可以得出以下结论:
(1) PPTL符号模型检测工具PLSMC是对CTL/LTL符号模型检测系统NuSMV的扩展,因此二者在对CTL/LTL公式进行验证时的时间开销与可验证系统规模基本保持一致.
(2) PPTL公式的范式转换过程需要消耗一定的系统时间,因此若将CTL公式使用对应的PPTL时序操作符进行描述,并使用PLSMC进行验证,其时间开销略高于直接使用NuSMV对CTL公式验证时的开销.
(3) PPTL引入了投影和投影星等时序操作符,因此PLSMC支持对NuSMV无法完整描述和验证的完全正则性质的检测.虽然使用PLSMC会引入额外的时间和空间开销,但是这种开销是可以接受的.
6 结 论本文分析NuSMV系统和PPTL符号模型检测方法的特点,提出了PPTL符号模型检测工具PLSMC的设计和实现过程.该工具不仅适用于硬件电路和嵌入式系统定性性质的验证,而且可以处理时间敏感性质、迭代性质和并发性质等定量性质;同时,可以有效缓解显式状态模型检测中容易出现的组合状态空间爆炸问题.
本文使用的PPTL公式范式转换工具pptl2nf有待改进,以克服性质公式较为复杂时转换过程较慢的问题.此外,PLSMC工具的用户界面和系统功能较为简单,因此在将来的工作中需要继续改进pptl2nf工具转换过程的复杂度,提高转换过程的效率;然后,完善PLSMC的用户界面,使其成为实际系统设计流程中实用的验证工具;最后,扩展PLSMC工具的功能, 使其可以同时支持PPTL的符号模型检测和限界模型检测方法,提高该工具可验证问题的规模.
| [1] | Clarke M, Grumberg O, Peled A. Model Checking. Cambridge: MIT Press, 2000. 35-49. |
| [2] | Kripke A. Semantical analysis of modal logic I: Normal propositional calculi. Mathematische Logik und Grundlagen der Mathematik, 1963,9:67-96 . |
| [3] | Wang ZM, Chen YY, Wang ZF. Automated theorem prover for pointer logic. Ruan Jian Xue Bao/Journal of Software, 2009,20(8): 2037-2050 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/572.htm |
| [4] | Yang Z, Ma GS, Zhang S. Equivalence verification of high-level datapaths based on polynomial symbolic algebra. Journal of Computer Research and Development, 2009,46(3):513-520 (in Chinese with English abstract). |
| [5] | Tian C, Duan ZH. Model checking proposition projection temporal logic based on SPIN. In: Butler M, Hinchey M, Larrondo-Petrie MM, eds. Proc. of the Int’l Conf. on Formal Engineering Methods 2007. LNCS 4789, Berlin, Heidelberg: Springer-Verlag, 2007. 246-265 . |
| [6] | Holzmann J. The model checker spin. IEEE Trans. on Software Engineering, 1997,23(5):279-295 . |
| [7] | Cimatti A, Clarke M, Giunchiglia1 F, Roveri M. NuSMV: A new symbolic model verifier. In: Halbwachs N, Peled D, eds. Proc. of the Int’l Symp. on Computer Aided Verification. LNCS 1633, Berlin, Heildelberg: Springer-Verlag, 1999. 495-499 . |
| [8] | Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. Nusmv 2: An opensource tool for symbolic model checking. In: Goos G, Hartmanis J, Leeuwen J, eds. Proc. of the 14th Int’l Conf. on Computer Aided Verification (CAV 2002). LNCS 2404, Heidelberg: Springer-Verlag, 2002. 359-364 . |
| [9] | Musuvathi M, Qadeer S. CHESS: A systematic testing tool for concurrent software. Technical Report, MSR-TR-2007-149, Redmond: Microsoft Research, 2007. 2-11. |
| [10] | Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In: Launchbury J, Mitchell JC, eds. Proc. of the Symp. on Principles of Programming Languages. Portland: ACM Press, 2002. 58-70 . |
| [11] | Ben-Ari M, Manna Z, Pnueli A. The temporal logic of branching time. Acta Informatica, 1983,20(1):207-226 . |
| [12] | Pnueli A. The temporal logic of programs. In: Young P, ed. Proc. of the 18th Annal IEEE Symp. on Foundations of Computer Science. Washington: IEEE Computer Society, 1977. 46-57 . |
| [13] | Wolper PL. Temporal logic can be more expressive. Information and Control, 1983,56(1-2):72-99 . |
| [14] | Duan ZH.Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2006. 9-104 (in Chinese). |
| [15] | Duan ZH. An extended interval temporal logic and a framing technique for temporal logic programming [Ph.D. Thesis]. Newcastle: University of Newcastle Upon Tyne, 1996. |
| [16] | Tian C, Duan ZH. Proposition projection temporal logic, Büchi automata and omega-expressions. In: Agrawal M, et al., eds. Proc. of the 5th Annual Conf. on Theory and Applications of Models of Computation. LNCS 4978, Berlin: Springer-Verlag, 2008. 47-58 . |
| [17] | Pang T, Duan ZH, Tian C. Symbolic model checking for propositional projection temporal logic. In: Proc. of the 6th Int’l Symp. on Theoretical Aspects of Software Engineering. Piscataway: IEEE Computer Society, 2012. 9-16 . |
| [18] | Bryant RE. Graph-Based algorithms for Boolean function manipulation. IEEE Trans. on Computers, 1986,35(8):687-691 . |
| [19] | McMillian L. Symbolic model checking, an approach to the state explosion problem [Ph.D. Thesis]. Boston: Carnegie Mellon University, 1993. 23-152. |
| [20] | Duan ZH, Tian C, Zhang L. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica, 2008,45(1):43-78 . |
| [21] | Somenzi F. CUDD: CU decision diagram package release 2.5.0. 2012. http://vlsi.colorado.edu/~fabio/CUDD/ |
| [22] | Fondazione Bruno Kessler. NuSMV examples: The collection. 2011. http://nusmv.fbk.eu/examples/examples.html |
| [3] | 王振明,陈意云,王志芳.用于指针逻辑的自动定理证明器.软件学报,2009,20(8):2037-2050. http://www.jos.org.cn/1000-9825/572. htm |
| [4] | 杨志,马光胜,张曙.基于多项式符号代数方法的高层次数据通路的等价验证.计算机研究与发展,2009,46(3):513-520. |