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