论文部分内容阅读
UML作为一种软件面向对象分析和设计的建模语言，已经得到了广泛的应用，但是，在软件的设计过程中，难免会引入一些错误。传统的软件测试方法是在软件开发完成之后进行的，而如果能够在软件开发早期对系统设计进行形式化验证，这样既能保证软件的可靠性，还可以提高开发效率，节约开发成本。模型检测技术是一种主流的形式化验证方法，目前已经在硬件和协议验证方面取得了成功，利用模型检测技术对软件进行形式化验证成为近年来研究的一个热点。 本文针对如何利用模型检测技术对软件设计阶段的UML模型进行形式化验证这一问题进行了研究，在汲取前人的经验和教训的基础上，提出了一套形式化转换规则，改进了一种UML模型动态特性的一致性验证方法，主要包括三个方面的工作: 首先，阐述了模型检测工具SPIN的工作原理和特点，分析了选取SPIN作为模型检测工具的优势，并且对其输入语言Promela和线性时态逻辑LTL进行了深入的分析; 其次，选取了一个包括类图、状态图和协作图在内的UML子集，从中提取系统的静态和动态信息，并且提出了一套形式化转换规则，将其转换为模型检测工具SPIN所支持的Promela模型，对系统进行验证; 最后，基于UML2.0顺序图所引入的交互片断，改进了一种UML模型动态特性的一致性验证方法，在此方法中，对状态图的形式化转换尝试使用基于XYZ/E的中间方法，通过验证状态图所对应的Promela模型是否满足顺序图所对应的LTL公式来达到验证一致性的目的。