论文部分内容阅读
UML是面向对象开发中一种可视化建模语言，已经成为事实上的面向对象建模标准。虽然表达丰富，但UML不是形式化的建模语言，其图形化的符号经常缺乏精确的语义，这使得对UML进行形式化推理十分困难。为了保证系统设计的正确性，在系统开发早期的时候发现可能存在的错误，进而降低系统开发的风险，对UML模型进行形式化验证很有必要。
本文选取了UML模型的一个包括类图、状态图、顺序图或协作图的的子集，研究了UML模型子集的NuSMV形式化语义，定义了UML语义向NuSMV语义转换的一系列规则，使得可以对半形式化的UML模型进行NuSMV形式化转换，并在此基础上加以形式化验证，对于形式化验证，本文采用了模型检测的方法。对NuSMV形式化验证的结果，本文进行了分析，并且讨论了如何将之转换为UML模型的逆向工程的方法，对此同样定义了将结果逆向工程到UML的一系列规则，使得能够对UML的形式化验证结果逆向转换为UML模型。本文还进一步设计并实现了基于上面转换规则的UML向NuSMV语义转换以及从NuSMV逆向到UML模型的转换工具，并将这两个方向的转换以及NuSMV模型检测工具整合在一个系统中，实现了对UML的自动形式化验证。
我们在BorlandTogether等环境中测试和验证本文定义的规则和实现的系统的正确性，分别建立两个不同应用领域的UML模型，利用我们实现的系统对两个实例进行NuSMV转换，并对NuSMV验证的结果逆向转换为UML模型，从而实现了对于给定实例的自动化验证。实际的测试与验证说明了该系统能够运用于软件开发的过程及其基于UML的开发环境与工具中。
论文的成果，不仅在理论上讨论了对半形式化UML模型语义的形式化及其逆向工程的一种可能性，而且在软件开发环境中实现了UML模型自动化验证的实例系统，这对于实际的软件开发过程也具有很强的实用意义。