随着计算机技术的发展,软件的复杂程度越来越高,对软件质量的要求也越来越严格。在软件开发过程中决定软件质量的一个重要步骤便是软件需求的描述和分析,由此便衍生出了软件工程的一个分支：需求工程。需求工程着重研究如何采用有效的工程化的技术和方法描述、并分析软件的需求,以获取高质量的软件需求。这便涵盖了两个方面的问题,即需求的描述和需求的验证。其中需求的描述是采用文档以及模型相结合的方法精确的描述目标软件系统所必须提供的功能和性能以及所要考虑的约束和限制。而需求的验证析则是在需求描述的基础上分析其完整性、正确性、可行性以及有效性等。这两个方面相互独立而又相辅相成,且处于同等重要的地位。随着需求工程的不断发展,一些新的理念和技术不断的被提出。例如在大型,复杂的软件系统需求分析中,将不可避免涉及到众多的有着各自背景、知识和职责的项目相关人员,于是便有了面向多视点的需求工程。面向多视点的需求采用“视点”的方式获取和组织不同的项目相关人员对系统不同的看法和要求,以构造其最终完整的需求描述。然而在这样一个研究领域之下却隐含着许多有待解决的问题,例如：1)如何建立基于多视点的需求规格说明；2)如何判断规格说明中多视点描述之间的不一致性；3)如何通过形式化的方法建立多视点的需求模型；4)如何在多视点的需求模型基础上验证需求的有效性等。对于前三者,本人所在的研究室均作了大量的研究工作,并提出了行为描述语言(BDL:Behavior Descriptive Language)。其中行为描述语言是一种基于多视点的形式化需求建模描述语言,其主要思想是通过目标系统所展现的行为来描述场景,并通过多个表示系统交互的场景来描述问题域中视点源所关注的视点。而在此基础上,本文主要研究使用BDL所构造的基于多视点以及软件行为的需求模型检测方法。通过对表示需求的行为模型做形式化的验证,以分析软件需求的有效性：即按照需求所实现的软件系统,是否与用户的期望一致。准确的说,本文将围绕传统的形式化验证的三个步骤：建立需求模型,构造系统特性以及检测模型是否满足特性,来讨论和分析基于多视点以及软件行为的需求模型检测问题。综上所述,本文主要做了如下工作：1)建模方法：简要概括了使用行为描述语言的需求建模方法,分析并讨论了行为描述语言的建模原理。2)建模语言：介绍了行为描述语言的基本语法,并从代数以及操作语义的角度,着重讨论了动态检测所必须的行为描述语言的语义。其中行为描述语言的类子以及操作被解释为一个抽象代数结构,称作行为∑代数,并在此基础上定义系统需求模型动态演变过程中的状态。系统模型的动态执行则被解释为状态的转换。3)特性描述方法：分析了目标系统特性与需求之间的关系,并提出了基于分支时序逻辑的系统特性规约描述语言：行为时序逻辑(BTL:Behavior Temporal Logic)。并在此基础上,提出使用设计模式(特性模板)的思想来描述系统特性,以适应非专业人员的使用,并增强特性规约的正确性,可读性,可重用性等。4)特性检测方法：对于检测方法,在构造了基于软件行为的需求模型操作语义模型的基础上,本文将划分为两类不同的情况分别加以分析。即系统功能相关特性的检测方法和质量相关属性的检测方法。其中功能特性的检测中,首先根据系统需求模型的操作语义生成状态迁移模型,并通过在该模型上构造BTL公式的解释合理性来验证模型是否满足给定的特性。此外,鉴于复杂系统模型中状态爆炸的问题,针对行为建模的特点,分析了检测优化的方法,其中包括基于视点封装特性的局部特性合成推理的检测优化方法以及基于命题泛化的检测优化方法。而在质量属性的检测中,利用了原子行为执行延迟呈指数分布,以及需求模型演变过程的马尔可夫特性,分析了系统的资源利用,行为吞吐量等质量属性。5)实例分析：最后本文研究了一个具体实例：网络图书销售系统。利用行为描述语言对其进行建模,并使用本文提出的方法验证了其一些关键的特性,并对验证过程进行了分析。