自适应软件是指通过感知运行环境的变化,及时调整软件运行状态或行为从而提供持续、高质量服务的软件。因此,自适应软件有效的增强了软件面对环境变化的能力以及自身的容错性,降低了软件维护成本。为了降低软件开发的复杂度,在设计阶段建立软件自适应模型并对模型进行验证是很有必要的。现有方法通常是利用UML(Unified Modeling Language)扩展机制构建软件自适应可视化模型(自适应序列图),由于可视化模型缺少验证所需要的形式化语义,因此,定义了转换规则与转换算法将其转换为具有精确语义的形式化模型(时间自动机网络),通过模型验证工具UPPAAL验证时间自动机。但现有方法在实际应用中还存在一定的不足,主要表现为:转换规则中部分模型元素在映射时出现语义概念混淆的问题,并且在实际应用中也存在问题,例如UPPAAL中存在四种类型的位置,现有方法仅定义了其中两种类型的转换规则,导致转换规则不够全面;另一方面,从自适应序列图到时间自动机网络的转换依赖于手动转换,并未实现自动转换,降低了转换的效率。对于验证失败后,也没有提供后续的处理机制,给设计开发人员带来不便。针对上述问题,本文研究的主要内容如下:(1)为解决现有转换规则中元素语义概念混淆的问题,本文对自适应序列图与时间自动机中模型元素语义进行全面分析,并针对实际情况将语义相近的模型元素进行对比映射,提出一组更为全面的转换规则,并实现了自适应序列图到时间自动机网络的自动转换算法,从而避免手动转换所带来的不便性,提高转换的效率。(2)为了简化形式化验证的流程,提高形式化验证的效率,本文根据模型验证工具UPPAAL中查询语言以及自适应软件的特性,提出一组软件自适应建模与设计过程中所需具备的性质,并进行规范化描述。通过UPPAAL对提出的性质进行验证用以确保软件自适应模型的正确性与可靠性。(3)为了便于设计开发人员得到正确的软件自适应模型作为可视化指导进行开发,本文提出从时间自动机网络自动转换为自适应序列图的自动转换算法,即在UPPAAL中修改验证失败的时间自动机直到验证通过,再将修正后时间自动机网络转换为自适应序列图,从而得到正确的自适应序列图,提高自适应软件开发的效率。(4)基于以上提出的两种转换算法,最后本文设计并实现软件自适应模型建模与转换工具M&C(Modeling and Conversion),并结合应用实例分析了工具的使用情况。