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