基于UML的建模及模型检验研究.pdf

2011年3月15日
现代电子技术
第34卷第6期
Modern Electronics Technique
Vol 34 No6
基于UML的建模及模型检验研究
吴晓丹,宁滨
(北京交通大学轨道交通控制与安全国家重点实验室、北京100044
摘要:UML是一种广泛使用的面向对象的可视化统一建模语言,但UML缺乏精确的语义描述,难以对UML.模型进
行分析验证以判断设计规范是否满足目标需求。符号模型检验是一种能够有效保证系统可信性质的自动捡验技术。为了
检验UMIL模型的正确性,在建模的基础上把UML模型转換为SMV模型,然后使用符号模型检验器(SMV)对模型进行检
验,有利于在系统的设计早期发现系统的缺陷。
关键词:UJML;符号模型检验;SMV;模型转换
中图分类号:TN919-34
文献标识码:A
文章编号:1004-373X(2011)06-0049-03
Modeling And Model Checking Based on UML
WU Xiao-dan, NING Bin
(State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China
Abstract: UML is a widely used object-oriented visual unified modeling language, but it is lack of precise semantics dis
cription. and difficult to analyze and verify the UML model so as to confirm if the specifications meet the desired requirement.
The symbolic model checking is an automated checking technique that can effectively ensure the system creditability. In order
to verify the correctness of the UMI, model, the UM]. model is translated to the SMV model, and then the symbolic mod
hecker is adopted to test the model. It is helpful to detect the system errors at the beginning of the design
Keywords: UML; symbolic modeling checking: SMV; model transform
究如何建立适合于SMV检验的UML模型,以及如何
0引言
把建立好的UML模型转换为用于檢验的SMV模型。
近年来,人们对软件正确性和安全性等可信性质关
注越来越多,要求愈来愈高,对于高可信的软件工程的1建立UML模型
研究也日趋重要。高可信软件工程技术是指获得和保1.1系统需求分析
证高可信软件系统关键性质的软件开发技术和过程技
系统需求分析是系统建模的第一步,需求分析完善
术。在建立软件系统模型的过程中离不开建模语言,随与否直接影响到建模的正确性及完备性。首先,用户把
着软件系统的规模和复杂性的日益增大,建模语言己经卡插入ATM机,然后再输入密码。系统判断密码是否
成为影响软件建模的关键因素。UMIL已成为面向对正确,如果不正确用户可以重新输人。如果用户连续
象的最流行的方法。大多数UML模型都是图形的且3次输入了错误的密码,ATM机将会吞卡。而如果用
易于理解。然而,UML没有提供一个验证模型正确性户输入了正确的密码,用户则可以按操作键来进行相关
的标准方法。
业务。该操作更新了包括可用余额在内的卡信息。用
模型检验作为一种形式化验证方法,近年来在各种户可以在任意时刻按退出键取卡同时产生一个错误
硬件、软件设计中得到了广泛应用们。这类方法的优点信号。
在于它有全自动化的检验过程且速度快、效率高,并且1.2建立UML类图
如果一个性质不满足,它能给出这个性质不满足的理
UML类图用于描述系统的静态结构,为后面的
由,据此可对系统描述进行改进。而后来符号模型检UML.状谷图的建模及模型转换打下基础。AIM系统
验技术的出现避免了内存爆炸问题,处理问题的规模也的类图如图1所示。该图在一般UML类图的基础上
随之増大。SMV是美国CMU计算机学院的 Mcmil-做了一些扩展。一是引人了 signal)和《send》)这
lanL.博土于1992年开发出的基于符号模型检验技术
两个类型的信号。分別表示类接收和发送的信号。如
的检验工具。本文主要通过一个自动取款机的实例研AIM类的( signal〉类型的 intropin()表示ATM接
收的信号,而〈〈send》〉类型的(k表示的则是ATM发
收稿日期:2010-11-23
送的信号。这样做的目的是为了更好地建立UMIL的