软件复用是在软件开发中避免重复劳动的解决方案。通过软件复用,可以提高软件开发的效率和质量。依据复用的对象,可以将软件复用分为产品复用和过程复用。其中,基于构件的复用是产品复用的主要形式,也是当前复用研究的焦点。给定一个基于构件的系统的有限状态模型和这个系统需要满足的性质,利用模型检测能够确定这个系统是否满足给定的性质,但模型检测中通常会遇到“状态爆炸”问题,其中组合推理作为一种基于检测局部状态空间的解决方法,它采用“分而治之”的策略来验证大规模系统。采用这种方法检测时,通常需要对每个组件的环境作出假定,这就是所说的假定-保证推理。本文围绕假定-保证推理重点展开,研究了如何使用假定-保证规则验证一个由n个组件组成的系统。主要内容包括：1.介绍了与本文相关的一些基本概念,包括软件复用和软件构件技术、形式化方法、模型检测、标记迁移系统、假定-保证推理等,另外重点描述了L*学习算法的过程,并且分析了它的单调性。2.总结了验证由n个组件组成系统的两种策略,分别是基于假定-保证规则ASYM和基于规则SYM-N的框架,并且分析比较了这两种框架。这两种框架都使用L*学习算法生成一个合适的假定判断系统是否满足性质,假定的生成过程是一个迭代的学习过程,往往为了得到验证结果,需要多次的学习过程。3.针对如何减少学习过程的迭代次数从而提高这些框架的效率,本文改进了基于规则SYM的学习框架,并且详细描述了这个框架对应的算法。这个框架同样使用L‘学习算法。但引入了等同反例和部分映像FSM的概念从而提高框架中L*学习算法的效率,另外通过改进框架的验证过程,在验证的过程中增加预判断操作等方法减少了原框架的迭代次数,提高了框架的效率。实验结果表明,改进后的框架与原框架相比具有更高的效率,并且分析了改进后框架的正确性及有穷性,即最终会运行结束并返回检测结果。