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