基于建模语言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;对于任何：

1.3 超时事件

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

2 模型验证工具SPIN

2.1 SPIN 概述

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

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

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

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

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中基本数据结构有：状态矢量，栈深度优先和已搜状态：

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

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

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

3 应用举例

3.1 使用实时UML建模

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.3 形式化验证

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

4 结论

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