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

Modeling And Model Checking Based on UML

作　　者：吴晓丹[1] 宁滨[1] 

机构地区：[1]北京交通大学轨道交通控制与安全国家重点实验室,北京100044

出　　处：《现代电子技术》2011年第6期49-51,54,共4页Modern Electronics Technique

摘　　要：UML是一种广泛使用的面向对象的可视化统一建模语言,但UML缺乏精确的语义描述,难以对UML模型进行分析验证以判断设计规范是否满足目标需求。符号模型检验是一种能够有效保证系统可信性质的自动检验技术。为了检验UML模型的正确性,在建模的基础上把UML模型转换为SMV模型,然后使用符号模型检验器(SMV)对模型进行检验,有利于在系统的设计早期发现系统的缺陷。UML is a widely used object-oriented visual unified modeling language, but it is lack of precise semantics discription, 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 UML model is translated to the SMV model, and then the symbolic model checker is adopted to test the model. It is helpful to detect the system errors at the beginning of the design.

关 键 词：UML 符号模型检验 SMV 模型转换 

分 类 号：TN919-34[电子电信—通信与信息系统]