论文部分内容阅读
随着计算机软件应用的深入,人们对软件的质量和可靠性提出了更高的要求.本文通过模型转换和模型检查的方法来验证软件模型的可靠性.首先通过Kripke结构将UML状态机的图形信息转换成NuSMV可以读取的SMV模型;接着在NuSMV模型检查工具中利用形式化语言CTL对生成的SMV模型进行检查,以验证软件系统的可靠性;最后本文以网上购物系统的订单模块为例进行了模型检查并作了改进,提高了系统的可靠性.