【摘要】 UML是一种广泛使用的面向对象的可视化统一建模语言,但UML缺乏精确的语义描述,难以对UML模型进行分析验证以判断设计规范是否满足目标需求。符号模型检验是一种能够有效保证系统可信性质的自动检验技术。为了检验UML模型的正确性,在建模的基础上把UML模型转换为SMV模型,然后使用符号模型检验器(SMV)对模型进行检验,有利于在系统的设计早期发现系统的缺陷。更多还原

【Abstract】 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 UML 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.更多还原