形式验证是提高软件可靠性的有效手段。为了控制形式验证特别是模型检验和精化检验的复杂性,研究人员提出了组合方法,其基水思想是“分而治之”,即把大的、系统整体的验证任务分解为一组小的、系统局部的子任务,再逐个解决。组合方法的一个关键问题是如何处理构件之间的相互依赖关系给任务分解带来的困难。因为传统的模型不能在构件的行为描述中显式地表达构件对环境的假设,因此在组合验证时往往需要单独构造环境模块,这较大程度地增加了组合验证的复杂性。本文研究基于一种新的形式模型——接口自动机来进行软件设计的组合验证、特别是组合精化检验的方法。这种新的形式模型支持在构件的建模中显式地表达它的环境假设信息,因而更有利于组合验证方法的使用。 本文对接口自动机模型的组合验证开展了三个方面的研究。首先,为了揭示这种新的形式模型的本质,本文研究了它与传统的I/O自动机模型之间的关系。然后在此基础上对接口自动机理论进行了完善,并研究了该理论在软件体系结构的组合分析与验证中的应用。最后,提出了接口自动机上的一种新的组合精化检验方法。 论文的主要贡献概括如下: 1.建立了接口自动机上的精化关系与I/O自动机上的前向模拟之间的等价关系。接口自动机的精化关系是以一种交替的(Alternating)方式来定义的,它与I/O自动机的前向模拟之间差别很大,以至于有的学者认为接口自动机和I/O自动机分别属于两类不同的模型(还有部分原因出自并发组合上的差异):接口模型和构件模型。上述等价关系的建立揭示了这两类模型之间存在的本质联系,从理论上确立了基于接口自动机的构件设计与基于I/O自动机的构件验证的集成基础,并使得利用I/O自动机的理论和工具来解决接口自动机的问题成为可能。 2.完善了接口自动机理论。这主要体现在三个方面。其一,发现并修正了原理论中的一个错误;其二,受进程代数CCS中的“2/3模拟”概念的启发,本文引入了接口自动机上的“2/3交替模拟”概念,这使得接口自动机的精化关系具备了保持“无死锁”性质的能力,从而增强了接口自动机的应用价值;其三,引入了广义精化的概念,来描述构件的接口与构件的实现之间的精化关系,并建立了相应的组合精化检验规则。 3.基于完善以后的接口自动机理论重新定义了软件体系结构描述语言WRIGHT的语义,新的语义解释更加简洁、更加自然。WRIGHT是一种著名的体系结构描述语言,它原来的测试规则(用于保证系统的协调性)比较复杂,这主要是因为在这些规则中必须