论文部分内容阅读
统一建模语言(United Modeling Language, UML)是一种描述功能强大且含义直观的可视化建模语言,它提供了多种图元,能够从不同角度和应用层次刻画系统特性,建模复杂的系统行为。基于UML的软件开发过程和建模环境已被学术界和工业界广泛接受,但是其图形化符号缺乏精确的语义描述,使得对UML模型进行正确性验证,以判断设计规范是否满足目标需求十分困难。因此,针对UML模型进行形式化描述与验证成为一个关键问题。本文以UML2.0模型为研究对象,提出了基于事件确定有限自动机(Event Deterministic Finite Automata, ETDFA)的序列图描述方法和基于命题投影时序逻辑(Propositional Projection Temporal Logic, PPTL)的序列图验证方法。以验证所得的自动机模型为基础,采用合成规则得到复合自动机,通过递增式测试用例生成算法获得测试用例的集合。为了确保分布式软件系统交互行为的正确性,研究了交互行为的建模、验证与测试方法,分别使用系统状态机图、对象状态机图和序列图对各模块状态变迁,以及模块之间的交互行为进行建模,通过验证与测试方法对所建立模型与交互行为的正确性进行确认。本文的主要贡献如下：(1)为UML2.0序列图提出了一种形式化描述方法。通过给出的序列图语法和语义定义,事件确定有限自动机的七元组定义,以及序列图的事件确定有限自动机构造算法来完成序列图的形式化描述过程。(2)采用基于命题投影时序逻辑的模型检测方法对描述序列图的自动机模型进行分析和验证。通过给出的基于ETDFA的PPTL模型检测算法得到验证结果,该方法可以在基于Spin的PPTL模型检测器的支持下得到实现。(3)分析现有的基于模型的测试用例生成技术,提出了一种递增式测试用例生成方法。在采用事件确定有限自动机描述UML2.0序列图建模的软件系统基础上,运用自动机合成算法得到相应的复合自动机,然后依次通过测试场景产生规则和测试用例集生成算法,递增式的产生测试用例集合。该方法能够提高所生成测试用例的正确性,同时降低生成过程的复杂性。(4)为了确保分布式软件系统中模块间交互行为的正确性,提出了一种通过系统状态机图、对象状态机图和序列图对各模块状态变迁以及模块之间交互行为进行建模的方法,采用基于命题投影时序逻辑的模型检测技术验证交互模型是否满足于系统性质,同时在验证所得序列图基础上,使用测试用例自动生成方法得到的测试用例集合能够实现对交互行为的有效测试。(5)给出了序列图到自动机模型转换工具的设计与实现。使用该工具能够完成UML模型和自动机模型的创建,以及序列图向自动机的自动转换。