需求问题的处理是软件项目成功与否的前提条件，软件需求工程的目标是采用系统化的方法和工程化的管理手段，为软件系统提供一个准确、安全、无二义性的开发文档。本文从面向方面文档驱动需求方法出发，在需求形式化描述方法、形式化需求建模过程、面向方面需求模型的一致性验证、需求变更影响分析几个方面进行了深入研究，提出了若干方法和算法。本文主要工作如下：1) Tabular表达式的指称语义定义。Tabular表达式是一种兼具数学的严谨性、规范性与可读性的形式化表示方法，针对Tabular表达式通用模型，给出了Tabular表达式的形式文法及指称语义。本文方法通过定义形式文法中各语法单元的语义指派方程描述了Tabular表达式的指称语义，并和其他几种Tabular表达式的语义描述方法进行了比较，分析表明，本文的语义描述方法不受Tabular表达式模型和Tabular表达式类型的限制，打破了现有方法的局限性。同时，语义的明确定义可以让用户更加精确的理解文档的含义，为后续形式化的分析与验证奠定基础。2)基于Tabular表达式的需求文档定义方法。本文使用Tabular表达式通用模型给出了4-变量模型的形式化描述。利用Tabular表达式通用模型描述4-变量模型中变量及变量间的关系,定义了从4-变量模型到Tabular表达式的映射规则；将Tabular表达式转换为逻辑系统，定义了一系列约束，并提出了需求完整性验证方法和可行性验证方法；对构建的Tabular表达式实例提出了软件系统的可接受性验证；本文使用灯控系统典型实例对本文的方法进行了验证，实验结果表明，提出的一系列方法可以有效地描述4-变量模型并对其进行软件可接受性验证。3)基于面向方面需求模型的完整性和一致性验证。本文针对面向方面需求方法给出了一系列提高建模准确度、检验模型完整性和一致性的策略和手段。首先，从需求依赖准确性、候选关注点分组可靠性和横切关注点判定三个角度给出了需求建模过程的验证策略；其次，给出了一个基于本体的关注点模型定义及验证方法，定义了基于本体的关注点模型，并定义了基于本体的关注点模型中完整性和一致性约束，介绍了从关注点模型到基于本体的关注点模型的映射规则及映射后的验证方法；最后通过一个实例验证了方法的可靠性，为设计和实现一个可靠的软件系统提供了有效信息。4)量化的需求变更影响分析方法。本文提出了一种基于可达矩阵的需求变更影响分析方法，从关注点和变量两个层面分别构建其关联矩阵和可达矩阵，并通过关注点重要度、关注点距离、影响程度、隶属相同和不同关注点变量间影响程度等定义，给出了一种计算需求变更波及影响范围和影响程度的量化算法。本文给出变更影响分析具有很好的连贯性，获得的量化结果可以为后续设计和代码编写提供有效的参考。