基于NuSMV的AUML模型形式化验证

摘要

多Agent系统(MultiAgentSystemMAS)是解决分布式复杂问题的一种重要手段，也是一种新的软件开发模式。为了适应多Agent系统的建模需要，B.Bauer等人在2000年提出了扩展的统一建模语言AUML。AUML虽然表达能力丰富，但却不是形式化的描述语言，其图形化的符号缺乏精确的定义，这使得对AUML所建立的系统模型难以进行形式化推理和验证。为了保证MAS系统设计的正确性，对AUML模型形式化语义转换并进行验证十分必要。 本文主要选取了AUML2.0的顺序图和交互概览图作为研究对象。为了有效地对AUML顺序图和交互概览图进行形式化验证，本文为AUML顺序图和交互概览图定义了一种可用于数据保存和交换的文本格式语言AODL，将AUML图形模型转换为AODL描述的文本；接着定义了一系列AUML到NuSMV的语义转换规则，并设计和实现了基于这些规则的转换程序，该程序以AODL文本为输入，以smv文件为输出，实现语义转换的自动化；最后本文用NuSMV检测器对转换得到的smv文件进行性质验证。通过两个协议实例的实验证明，本文定义的语义转换规则是有效的，形式化验证AUML2.0模型图是可行且有效的。 本文的成果，不仅定义了一系列从AUML2.0到NuSMV语义的映射规则，实现了一个将AODL所描述的AUML图模型转换为NuSMV模型的转换程序，并用NuSMV检测了AUML模型的性质，通过检测有助于指导建模者建立更加精确的模型；而且定义了一种可以描述AUML顺序图和交互概览图的数据交换格式语言AODL，通过这种AODL语言可以将AUML顺序图和交互概览图的图形模型保存为文本格式，也使得在不同的应用之间交换AUML数据成为可能；本文还通过实验证明了形式化验证AUML2.0模型的有效性和正确性，这对于实际的MAS开发过程具有一定的实用意义。

目录

文摘

英文文摘

第1章 研究背景与问题陈述

第2章 AUML与NuSMV语义分析

第3章AUML的NuSMV语义转换

第4章 AUML交互图定义语言的形式化定义

第5章 AUML向NuSMV语义转换工具的设计与实现

第6章 AUML 2.0语义转换的实例及验证

第7章 问题总结与展望

参考文献

附 录

致谢

原创性声明