基于UML 的嵌入式系统模型验证技术的研究

　　摘要：统一建模语言UML 在嵌入式系统设计建模中已经获得了广泛的认可，能对复杂嵌入式系统建模，并有很多成功的应用，但UML 是一种半形式化语言，存在时间约束描述能力不强和所建模型形式化复杂.验证难度大等问题.针对上述问题，本文提出了采用实时UML 对嵌入式系统UML 状态图进行建模；然后用状态- 约束- 事件矩阵方法来对模型进行形式化描述；利用SPIN 对模型进行验证.该方法解决了UML 在嵌入式系统建模和形式化验证过程中出现的问题，应用实例和结果证明了该方法的有效性和可行性.

　　0 引言

　　随着对嵌入式系统复杂性和应用需求的无限增加，其系统软件开发的工作量剧增.统一建模语言UML 已在嵌入式系统建模中得到广泛应用.UML 能够直观易懂的描绘出系统的需求.功能.结构及相应的行为，另外，使用UML 有助于企业相互交流，克服沟通障碍.

　　然而在该领域还存在一定问题，首先UML 对时间约束描述能力不强；其次UML 为非形式化语言，其所建模型形式化转换复杂.目前已有解决办法： 使用UML 的扩展机制；使用分析模式.然而扩展机制是建模人员自己定义的，容易增加UML 整体的复杂性；形式化转换复杂，需要特殊工具支撑.

　　为了更好的解决上述问题，论文采用实时UML 对嵌入式系统建模； 状态- 约束- 事件矩阵方法对模型进行形式化描述；利用SPIN 对模型进行分析和验证.

　　1 实时UML 描述嵌入式系统

　　1.1 实时UML 概述

　　实时UML 主要由Rational 公司开发.它合并了UML?角色建模.ROOM 中的概念，开发出一个新的.比较完善的可用于复杂实时系统建模的标准.实时UML 中主要引入三个概念.

　　端口：随着胶囊事例的创建.消亡而同步运作.

　　连接器：基于特定协议的信号传递通路.

　　胶囊：表示复杂实时系统中的主要结构元素.

　　1.2 UML 实时状态图的形式语义

　　实时状态图D = （A,T,F,G,Time,aL ,aF ）.其中 A:有限状态集 ;T :有限转移集；F ∈（A×T）∪（T×A）是流关系 ;G（t） :条件表达式 ;Time :某个状态迟完成的时钟时间 ;a L ∈A :初始状态，a F ∈A:终止状态 ;只有一个转移 t 满足  （ a L, t）∈ F;对于任何：

　　3 超时事件

　　为实时状态图D 中的超时事件加入时间约束：对于集合T中的任意元素t,若G （t） 为真，与t 相对应的截止期为d（t）=2?

　　对于所有进入状态t<b（t） 的转移，加入时钟约束（x=0） ;对于所有的从该状态出发的转移，加入时钟约束（x<2）.

　　2 模型验证工具SPIN

　　2.1 SPIN 概述

　　SPIN 主要包括模型仿真器和模型分析器两个主要功能：模型仿真器可以快速对所建立的系统模型进行仿真；模型分析器可以严格地验证用户提出的正确性要求是否被满足.SPIN 作为一种形式化自动验证工具，目的是提供：

　　2.1.1 建模语言PROMELA: 直观地描述系统规约；

　　2.1.2 功能强大而简明的逻辑表示法LTL ;

　　2.1.3 可验证系统建模逻辑一致性及系统是否满足所要验证性质.

　　2.2 线性时序逻辑LTL

　　SPIN 用线性时序逻辑LTL 性质描述系统的性质.采用线性.离散.与自然数同构的时间结构.以状态序列作为命题的论断对象.用线性时序逻辑公式在状态序列上解释其真值.语法可递归定义如下：

　　定义1 :命题常元{true , false} 和原子命题变元{p,q,…}

　　是线性时序逻辑公式.

　　定义2 :如果p 和q 是线性时序逻辑公式.则p（sometimes） p∪q（until） p ∨ q（or），p ∧ q（and） 非p（not）/ p（always） Xp（next）也是线性时序逻辑公式.

　　2.3 基本数据结构

　　在SPIN 中基本数据结构有：状态矢量，栈深度优先和已搜状态：

　　2.3.1 状态矢量：包括全局和局部变量；

　　2.3.2 栈深度优先：指出回溯方向和引起违反的状态迁移序列；

　　2.3.3 已搜状态：达到减少状态压缩.提高搜索效率的目的.

　　3 应用举例

　　3.1 使用实时UML 建模

　　对嵌入式系统进行模型验证的步骤为：

　　1  用实时UML 为嵌入式系统建模；

　　2. 根据所建模型构建状态- 约束- 事件矩阵；

　　3. 根据矩阵的形式化描述，用Promela 编写系统程序；

　　4. 用XSPIN 系统验证程序的正确性和可行性；

　　5. 根据错误迹修改模型.下面以自动售货机为例，讨论如何建模和验证.

　　自动售货机系统由初始化模块.投币模块.找零模块.出货模块.超时退钱模块组成执行步骤为：

　　1  系统初始化，等待顾客来购买；

　　2. 顾客选择所要购买的商品；

　　3. 根据系统提示的价格进行投币；

　　4. 系统对顾客所投的钱与商品单价进行比较；

　　5. 大于则找零.相等则系统出货.不足提醒顾客继续投；

　　6. 若顾客投币不足，且不想继续购买，则系统进行超时退钱.对应的UML 状态图如图1 所示：

　　3.2 模型形式化

　　描述为了能形式化表达自动售货机状态图的时间约束，该系统中可能发生的迁移.时间约束和发生条件用状态- 约束- 事件矩阵来表示.状态- 约束- 事件矩阵被认为是用来描述嵌入式系统行为的抽象概念.自动售货机系统对应的部分状态约束事件矩阵如图2

　　3.3 形式化验证

　　运行程序时，首先进行语法检测和冗余检测.冗余检测时会给出一些改进模型的建议.如果在运行中发现一些给定参数的状态没有正确达到，这些语句将被反显在主窗口中，并给出验证输出窗口，如图3?根据提示可以确定错误类型.错误类型包括违反断言.死锁.无效循环等，图3 可以看出错误为违反断言.

　　4 结论

　　近年来，关于UML 与模型检测结合的研究一直十分活跃，但是这方面的技术还不够成熟.首先，一些国内外着名的研究高校都在进一步研究和发展这种技术，这些研究机构把提高UML 语言的性，研究UML 模型转换和开发UML 的支撑工具作为当前的研究重点.其次，在众多已经流行的模型验证工具中，SPIN 是获得ACM 软件系统奖的工具，已经成功应用在控制系统验证.安全协议验证.化规划等领域.SPIN 内嵌了很多用于状态空间压缩的优化算法，但模型校验器仍然需要很长的时间才能验证一个指定的属性，所以，状态爆炸问题仍是一个令人头疼的问题.