提高软件可靠性是软件开发的重要课题之一。软件可靠性手段包括分析、测试和验证等,其中测试的投入往往占系统开发总成本的很大比例,因此测试效率的提高可以有效缩减成本。但测试面临很多难题,比如软件测试自动化程度的提高、非功能属性的测试、并发软件的测试等。　　 软件生命周期的各个阶段都会涉及到不同的模型。软件模型提供了通用的交流平台,使得系统开发的不同角色可以进行信息交互。比如,需求模型是客户和系统分析人员的桥梁,设计模型是设计人员和开发人员的沟通工具。模型代表了设计者对软件系统的预期,可以成为测试的基准;同时,软件模型包含大量的功能和结构信息,为测试用例的生成提供依据。　　 本文回顾了面向对象建模技术和构件系统模型,对统一建模语言UML及其中的活动图、顺序图和状态图作了形式化分析,为后续的研究奠定了基础。针对基于模型的测试中存在的重要问题,开展了测试用例生成和测试结果自动分析等方面的研究,提出了基于UML动态模型的解决方案,包含以下几个方面的工作:　　 1.提出一个基于状态机的构件健壮性测试方法。基于形式化的构件语义定义了构件健壮性。在此基础上开发了构件健壮性测试框架,首先遍历状态机生成一组覆盖所有转换的路径,基于这些路径生成健壮性测试用例;生成的用例首先用带有有效输入的方法调用序列驱动被测构件,让它按照生成的路径发生状态转换,然后用无效输入和不当调用在构件的不同状态来测试其健壮性:通过区分测试中捕获异常的类别,自动报告健壮性错误。　　 实现了原型工具RoTesCo,选定一组开源软件组成测试平台;并实现了随机测试方法和基于状态的功能性测试方法,与RoTesCo在同一平台上进行测试,通过结果比较验证了本文提出方法的有效性。　　 2.提出一个基于活动图的Java并发程序的数据竞争检测方法。用扩展了数据访问标记的UML活动图描述程序的行为模型;基于活动图插装被测试程序以获取程序执行轨迹;用基于路径分析生成的测试用例来执行插装后的程序;对轨迹反向工程可以得到数据访问事件列表,通过检验不同线程进入和退出关键区的时间是否重合来发现数据竞争。　　 实现了原型工具Toc4j,并进行了实例分析,验证了提出方法的有效性。　　 3.提出一个基于UML动态模型的运行时验证方法。分析了UML动态模型中顺序图、活动图和状态机的属性;利用这些动态模型进行测试用例的生成和程序插装,运行插装后的程序获取执行轨迹;再以模型为规约进行一致性检验,验证程序实现是否与模型一致。其中顺序图用于描述对象之间的消息发送和接受;活动图用于描述程序的控制流程和共享数据的访问;状态机用于描述被测软件接受消息的时序。　　 设计了基于动态模型的运行时验证框架,并对这几种模型分别进行了算法实现和实例分析。