需求验证一直以来都是软件开发过程中非常重要的一个环节，软件需求的正确性直接影响着后期开发工作中人力、物力和资源的消耗。随着网络技术的发展，一种部署在网络环境中的复杂软件系统—网络式软件产生了，其拓扑结构和软件行为可以动态演化，因此，对传统的需求验证方法提出了新的要求。形式化方法通过对系统进行严格的语法和语义定义，使得分析和推理能够精确化、数学化，从而能够完备的证明系统是否正确实现了设计者的意图。网络式软件需求模型的验证主要针对目标模型和过程模型，在973项目“需求模型验证与管理”（2007CB310803）的支持下，本文针对网络式软件需求模型目标层和过程层的特点，充分利用已有的形式化规约语言和分析方法对其进行形式化方法的研究。主要工作包括以下几个方面：1.针对因网络式软件复杂性而带来的需求获取信息不协调性难以避免的特点，提出应用极大协调子集的思想进行不一致信息的处理；针对处理后的信息，在目标层模型思想的指导下，建立了一种新的描述需求目标性质和目标之间关系的GM模型，给出了GM模型正确性和完整性分析方法，以及相关验证算法，并设计了动态环境下目标模型演化的相关规则。该方法可以刻画目标层中所有目标之间的关系，包括低层目标之间的关系和高层目标之间的关系，并能融合用户需求之间的不一致信息，保留需求初期还未能确定的系统目标。2.在深入研究Z语言和Petri网特点的基础上，扩展了集成Petri网和Z语言的PZN模型，并将它应用于网络式软件需求过程模型的建模分析，给出了PZN模型的活性、可达性和完整性具体分析方法，基于PZN模型对过程模型进行形式化建模和分析，利用PZN中所含的Petri网性质分析过程模型的活性和可达性，通过PZN中的Z框架描述分析过程模型的完整性，同时，给出了动态环境下，过程模型的增加、减少、模块划分等变化规则。3.为了保证过程模型同已确认的需求目标及业务规则的一致性，在分析原子目标和原子过程的映射关系的基础上，分析了整个目标模型与过程模型间的相互关系，提出了目标层与过程层的一致性定义及其分析方法，以保证过程模型能够正确的实现用户需求目标，以及需求分析过程中目标与过程的统一。本文在网络式软件需求验证的形式化方法上的研究成果，能有效的刻画用户需求的功能属性和非功能属性，有利于提高需求分析阶段的正确性和完整性，降低软件中因为用户需求的不正确而带来的错误以及资源的损失，提高软件开发的效率。同时，本文作者参与了所在团队网络式软件需求模型验证器的开发，实现了本文中的需求验证方法，并对项目实例进行验证，实例显示本文的方法具有很好的效果。