智能的UML模型的形式化检测方法及装置

摘要

本发明提出一种智能的UML模型的形式化检测方法及装置，该方法包括：对真实系统建立UML模型，并将UML模型转换为XMI模型；从XMI模型中提取预定元素信息，并应用一套转换规则对预定元素信息进行语义转换以得到SMV模型；获取CTL和/或LTL命题逻辑检测式，其中，CTL和/或LTL命题逻辑检测式用于对SMV模型进行模型检测；根据CTL和/或LTL命题逻辑检测式和SMV模型构建二叉决策图以对SMV模型进行检测以得到检测结果。根据本发明的实施例，具有检测准确性高、且能够对安全性有较高要求的软件开发过程中的UML模型进行综合性检测，应用面广的优点。