资源描述：
《UML模型检测方法的研究》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、第27卷第10期计算机应用Vol.27No.102007年10月ComputerApplicationsOct.2007文章编号:1001-9081(2007)10-2493-05UML模型检测方法的研究张频,罗贵明(清华大学软件学院,北京100084)(pin-zhang04@mails.tsinghua.edu.cn)摘要:统一建模语言(UML)是设计和分析软件系统最常用的方法,如何保证UML模型满足某些特性是一个非常重要的问题,而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器(
2、SPIN)对UML模型进行检测的方法。首先对UML模型进行形式化描述,使用层次自动机来描述状态图,然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA,使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束,通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。关键词:模型检测;统一建模语言;层次自动机;简单进程元语言解释器;PROMELA中图分类号:TP311.5文献标志码:AResearchofm
3、odelcheckingUMLZHANGPin,LUOGui2ming(SchoolofSoftware,TsinghuaUniversity,Beijing100084,China)Abstract:UnifiedModelingLanguage(UML)isthemostcommonlyusedmethodinsoftwaresystemdesignandanalysis,andhowtoverifythattheUMLmodelsatisfiessomepropertiesisaveryimportantiss
4、ue.ModelCheckingisanefficientautomatictechniquefortheimprovementofsystempsreliability,andthispaperisaresearchintohowtocheckUMLmodelthroughtheSimplePROMELAInterpreter(SPIN)model2checker.AfterdescribingtheUMLmodelusingformalmethod,wefirstusedhierarchicalautomatat
5、oexpressstatechartsdiagram.Inaddition,wetranslatedthestatechartsandpartoftheclassdiagramintoPROMELAbasedontheoperationalsemanticofhierarchicalautomata,andverifiedthemodelbyusingSimplePromelaInterpreter(SPIN)totestifitsatisfiedtheLTLproperties.Wealsoverifiedthec
6、onsistencybetweensequencediagramandstatechartsdiagrambyusingLTLformulatoexpresssequencediagram.Finally,basedonthemethod,wedevelopedamodelcheckertoolcalledUMLChecker.Keywords:modelchecking;UnifiedModelingLanguage(UML);hierarchicalautomata;SimplePROMELAInterprete
7、r(SPIN);PROMELA模语言PROMELA是一种代码语言,通过PROMELA精确描0引言述系统不是一件很容易的事情而且很不直观,相比之下,图形[1]模型检测是验证有限状态系统的自动化技术,能够有化的建模方式则具有不可替代的优势,统一建模语言(Unified效地提高系统的可靠性。模型检测主要三部分工作:对系统ModelingLanguage,UML)就是其中之一,它是用来对面向对[4]进行形式化建模、精确表达系统约束以及验证模型是否满足象系统进行设计和分析的标准语言。UML模型中定义了给定约束,如果不满足则列出
8、错误轨迹,通过对错误轨迹的分不同的视图从不同的侧面描述系统的静态结构和动态行为,析便可得出系统的错误所在。模型检测所使用的形式化建模包括:用例图、顺序图、协作图、类图、对象图、状态图、活动图、结构Kripkestructure是一种类似于自动机的状态转换图结构件图和部署图等九个视图。UML已经广泛用于各种软件[1]构。系统属性的描述方法通常采用
