随着计算机软硬件技术的高速发展，人们对其安全性和可靠性的要求越来越高[1-2]．传统的软件测试只能找出软件中可能存在的问题，不能验证软件的正确性．模型检测作为形式化验证的方法，以其高度自动化的特点受到了工业界和学术界的关注，被广泛应用到计算机软硬件安全性、可靠性的验证[3-4]．模型检测首先将待验证的系统抽象为一个有穷状态迁移系统模型，使用不同的时态逻辑对系统属性进行描述，通过模型检测算法验证模型是否满足属性，若满足，则返回TRUE；若不满足，则返回FALSE并给出一条不满足的路径，以供后续软件开发人员对系统做出相应修改．虽然模型检测有诸多优点，且在软件开发初期对软件需求进行形式化验证可以有效地找出系统中存在的问题[5]，但是模型检测须要结合某种特定的形式化规范逻辑对验证系统进行形式化描述，建立形式化模型，使用难度较大．统一建模语言(unified modeling language，UML)是目前应用非常广泛的一种可视化面向对象建模语言[6]，可用于很多复杂系统的设计，已经成为一种国际标准建模语言[7]．将UML技术与形式化方法相结合，国内外许多学者已经进行了相关的研究．文献[8]通过将UML中活动图形式化的方式，展示了一个系统形式化的过程，得出了形式化方法可以提高分析和开发系统能力的结论．文献[9]对汽车防碰撞系统进行了UML建模，提出了部分转换规则，并将需求分析模型转换为形式化模型．文献[10]对铁路车站的计算机联锁系统进行了需求分析并建立了UML模型，给出了部分转换规则且在最后通过NuSMV，对系统的属性进行了验证．本研究首先使用UML对系统进行需求分析，建立系统的UML模型[11-12]，然后将UML模型转化为新符号模型检测器(new symbolic model verifier，NuSMV)模型以供后续进行形式化验证[13-17]，最后通过一个电梯系统的建模、转换与验证给出示例．1 UML模型建立并发系统是由一组(部分)独立的子系统组成的．整个系统的状态空间由各个子系统的状态空间构成，并且系统整体的迁移动作也由子系统的迁移动作组成．系统的并发性由同时执行的子系统之间迁移动作的非确定性选择体现[18]．如果系统的各个子系统完全独立，那么系统的运行方式为完全随机的异步转移；如果系统的子系统之间存在一定的关联，那么可能会通过共享变量或握手等机制进行子系统之间的通信或同步．电梯控制系统是由楼层控制模块(Landingcontrol)、开关门模块(Opendoorbut，Closedoorbut)、电梯楼层控制模块(Liftcontrol)、电梯厢模块(Lift)和超重模块(Overweightchek)构成的并发系统．当电梯运行时，除电梯厢模块外，其他模块各楼层间随机发生对电梯的请求、电梯开关门等，电梯厢模块与其他模块通过握手动作进行信息的传递，即电梯厢会根据某时刻其他模块对电梯的请求而发生状态迁移．利用UML的类图、状态图和顺序图分别描述系统整体的静态结构、系统的动态行为、对象之间消息的交互[19-20]．以一个双按键电梯控制系统为例，使用Enterprise Architect建立UML模型．建立类图时，首先将系统的模块作为类图中的类，然后确定类的属性、操作及类之间的关联关系．电梯控制系统的类图如图1所示．10.13245/j.hust.240212.F001图1双按键电梯系统类图建立状态图，首先要明确每个类对象可能存在的状态及可转移的两个状态之间的转移条件．例如电梯系统按键状态图(图2)．10.13245/j.hust.240212.F002图2电梯系统按键状态图状态转移条件TRUE代表除选择结构中其他条件外的所有情况，用于模拟按键被随机按下．电梯中按键的状态初始设为FALSE，随机的被使用者按下(经过条件TRUE发生转移)后变为TRUE且该按键的请求没有被满足前保持被按下的状态，请求被满足后重置为FALSE．电梯系统模型中各按键模拟电梯在日常使用中的情况，按键被按下后通过握手动作产生相关变量的传递，对电梯厢运行产生影响．当电梯系统中对电梯厢产生请求的事件发生时，各子系统会通过握手方式与电梯厢模块产生通信，决定电梯厢的状态迁移．电梯厢模块通过握手机制与电梯楼层控制模块进行通信．建立UML顺序图，列出参与事件类所对应的对象．双按键电梯系统的顺序图仅用于描述某一模块对其他模块的加载．以电梯控制系统顺序图举例(图3)．10.13245/j.hust.240212.F003图3电梯控制系统顺序图2 UML-NuSMV模型转换算法2.1　类图转换规则及算法面向对象建模语言UML中类图的定义与NuSMV中模块的定义相似，都是将每个子模块以实例化的方式进行描述．当模型转换时，从XML文件中读取类图中的信息，依次完成各模块的转换，类图转换规则如下．a．类图中类名转换为NuSMV中模块名．b．类图中属性的属性名及属性类型转化为NuSMV中的变量名及变量类型，其中char类型属性转换为枚举类型变量，变量取值从相应状态图中提取．c．类图中构造方法的参数转换为NuSMV中模块的参数．d．若类中属性有初始值，则将其转化为NuSMV中ASSIGN部分变量的初始化．在进行两种模型之间的转换前，通过Enterprise Architect将UML模型输出为XML格式的可读文本，并通过DOM接口对文件进行解析．具体实现方式如算法1所示．算法1 类图转换算法输入 输出为XML格式UML模型文件输出 字符串1(NuSMV模型的声明)，字符串2(NuSMV中ASSIGN部分的属性初始化)，字符串3(NuSMV中变量的定义)步骤1 读取XML文件中UML：Class标签，将标签以列表的形式保存在classes中，遍历列表，获取类名及操作名，并保存于cn，mn中，若两者值相等，则读取parameter name的值保存于clp中，将"MODULE"，cn+"("+clp+")"赋值给字符串1．步骤2 读取attribute name及value的值并保存在atn与att中，若att的值为"char"，则读取状态图中状态的取值保存在att中，将atn+"："+att赋值给字符串3．步骤3 读取attribute标签下标签为UML：Expression的第一个孩子节点并保存在ini中，读取标签节点属性body的值，将值保存在init中，若init不为空，将"init("+atn+")：="+init赋值给字符串2．返回 字符串1，字符串2，字符串3．2.2　状态图转换规则及算法在UML模型中，状态图的建立依附于类图，因此转换状态图时，要将状态图中的状态转移对应到其从属的类中，并且最终转换到对应的NuSMV子模块中．状态图的转换规则如下．a．状态图中状态的转移条件转换为NuSMV中变量状态转移的条件．b．状态图中转移的目标状态，转换为NuSMV中变量转移的目标．为了区分某个转移与状态图的从属关系，须要读取状态图、转移、状态三者的标签id，具体实现如算法2所示．算法2 状态图转换算法输入 输出为XML格式UML模型文件输出 字符串1(状态转移的初始说明)，字符串2(状态转移条件)步骤1 读取XML文件中UML：Class标签，将标签以列表的形式保存在classes中，遍历列表，读取attribute name的值保存在atn中，读取attribute标签下标签为UML：Expression的第一个孩子节点并保存在ini中，读取状态图包下标签为UML：Package的值并保存在列表statepackges中．步骤2 遍历列表statepackges，读取XML文件中UML：Class标签将标签以列表的形式保存在classes中，读取标签属性body及value的值保存在gc与e中，将gc+"："+e赋值给字符串2，若init为空，则将"next("+atn+")：=case"赋值给字符串1，若不为空，则将atn+"：=case"赋值给字符串1．返回 字符串1，字符串22.3　顺序图转换规则及算法顺序图用于描述系统模块之间的信息交互，在双按键电梯系统中主要用来表示某模块对其他模块的加载．NuSMV中的main模块被用来描述系统的交互框架及一些全局变量的定义，因此当转换顺序图时，若搜索到电梯控制顺序图，则读取其中的信息，创建NuSMV中的main模块．顺序图转换规则为读取两个对象之间传递消息的目标及消息的参数，转换为NuSMV中某个模块对其他模块的加载．算法3实现顺序图的转化规则．算法3 顺序图转换算法输入 输出为XML格式UML模型文件输出 字符串1(顺序图中消息传递的目标)，字符串2(消息传递中的参数)步骤1 读取XML文件中标签UML：Interaction.message第一个孩子节点，读取节点下UML：Message标签，将标签以列表的形式保存在messages中，读取标签属性xmi.id的值并保存在mgid中，读取message标签下标签UML：TaggedValue标签并遍历列表，读取标签属性tag的值保存在ftag中．步骤2 若ftag的值为"ea_targetName"，则读取标签属性value的值并保存在tar中，若ftag为"privatedata2"，则读取标签属性value的值，保存在tap中．步骤3 读取XML文件中标签UML：Diagram的值，保存在sqs列表中并遍历列表，读取标签属性subject的值，将值保存在subid中，若subid的取值与mgid相同，则将tar赋值给字符串1，将tap赋值给字符串2．返回 字符串1，字符串2XML文件标签为一种嵌套结构，当算法在读取XML文本中信息时，采用递归的方式进行搜索．算法1中，设UML：Class标签与UML：Operation标签共有c1和c2个，XML文件中第一个UML：Operation标签下第一层有n个UML：Parameter标签，并且最坏情况下每个节点下一层都有n个节点，XML标签嵌套结构的平均层数为h，那么遍历UML：Parameter标签须读取一棵n叉的完全树，n叉完全树节点应有(1-nh)/(1-n)个，读取标签节点的次数为c1c2(1-nh)/(1-n)次．设每次读取时间复杂度都为1，那么算法时间复杂度为O(nh)．算法2，3复杂度与算法1相同，主要受所读取标签个数及XML文件嵌套层数的影响，当n为遍历一个标签时须读取的n叉完全树时，算法时间复杂度均为O(nh)．3 系统属性的描述首先结合计算树逻辑(computation tree logic，CTL)对需求分析阶段系统的属性进行描述，然后利用NuSMV对系统状态空间进行搜索，以判断系统是否满足编写的CTL公式．CTL由状态公式和路径公式两部分组成，路径公式中量词A表示对所有路径而言，量词E表示对任意一条路径而言，状态公式的量词有X，U，F，G．若设命题变量p和q为表示系统状态的公式，则Xp表示当前状态的下一个状态满足p，pUq表示直到满足q之前的所有状态都满足p，Fp表示未来会存在一个状态满足p，Gp表示所有的状态都满足p．在系统的需求分析阶段对系统进行形式化验证，主要通过形式化的方式分析检测系统的需求是否存在逻辑上的冲突与错误，并检查根据需求建立的系统模型是否存在安全问题．针对双按键并发电梯系统，假设其验证的属性有8个．属性1 按下楼层间的按键，电梯将会到达该楼层，并打开电梯门，CTL公式为AG (landingcontrol1.landingBut2U.presse-AF (lift1.floor=2 & lift1.door=open))．属性2 按下电梯厢的楼层按键，电梯将会到达该楼层，并将电梯门打开，CTL公式为AF(liftcontrol1.liftBut4.pressed-AF(lift1.floor=4 & lift1.door=open))．属性3 当电梯在当前运行方向上有对电梯的请求时，电梯在到达请求位置之前，运行方向不会发生改变，CTL公式为AF((lift1.floor=2 & liftcontrol1.liftBut5.pressed &lift1.direction=up-A[lift1.direction=upUlift1.floor=5]) & (lift1.floor=6 & liftcontrol1.liftBut3.pressed & lift1.direction=down-A[lift1.direction=downUlift1.floor=3]))．属性4 如果电梯处于超重状态，那么电梯保持静止且电梯门打开，CTL公式为AG(overweightcheck.overweight=TRUE & lift1.floor=3-(lift1.floor=3 & lift1.door=open))．属性5 电梯可能在没有对电梯请求的情况下，在第某层保持静止，且电梯门关闭，CTL公式为AG (lift1.floor=1 & liftcontrol1.idle & lift1.door=closed-EG (lift1.floor=1 & lift1.door=closed))．属性6 按下电梯的开门按键，电梯门会在可以打开的情况下打开，CTL公式为AG (liftcontrol1.opendoorbutton.pressed-EF(liftcontrol1.opendoorbutton.judgeopenok & lift1.door=open))．属性7 按下电梯的关门按键，电梯门会在可以关闭的情况下关闭，CTL公式为AG (liftcontrol1.closedoorbutton.pressed-EF (liftcontrol1.closedoorbutton.judgecloseok & lift1.door=closed))．属性8 当电梯在运行时，电梯门一直保持关闭，CTL公式为AF ((!liftcontrol1.idle & lift1.floor!=liftcontrol1.lift_call & lift1.floor!=landingcontrol1.landing_call)-AF(lift1.door=closed))．4 系统属性的验证通过NuSMV对双按键并发电梯系统的8个属性进行自动化验证，结果如表1所示．10.13245/j.hust.240212.T001表1验证结果属性BDD Nodes/105结果12.293 55FALSE21.757 57TRUE33.076 74TRUE41.652 42TRUE51.676 29TRUE61.993 79TRUE71.953 57TRUE81.735 88TRUE当系统不满足属性1时，NuSMV给出反例路径如下所示．-State：1.2-…overweightcheck.alarm=TRUEoverweightcheck.overweight=TRUElift1.door=open--Loop starts here-State：1.3-…-State：1.4-由路径可知，电梯在某时刻，因为一直处于超重，进入了一直保持不动且将电梯门打开的状态．这种情况是符合预期的．若电梯处于超重状态不发生改变，电梯理应保持静止，且将电梯门打开，符合对电梯系统的安全性要求．若验证系统能否在任意路径下都有一个状态使得楼层间的电梯请求得到满足，则将表时序的量词改为F，排除电梯一直保持超重的状态即可，CTL公式为AF (landingcontrol1.landingBut2U.pressed- AF (lift1.floor=2 & lift1.door=open))经验证系统满足该属性．5 结语为解决形式化验证时系统的形式化模型描述问题，本研究提出了结合UML技术建立系统需求分析模型并将其转换为形式化NuSMV模型的一种方法，在此基础上，编写了系统的待验证属性，完成了系统的形式化验证．