随着计算机技术应用的日益广泛，目前在国内外航天飞行器上采用软件实现的功能越来越多，软件的规模也越来越大。通过对航天计算机系统的软件所普遍存在着的错误进行分析，结合一些实际数据，我们清晰地看到，软件需求规格说明常常是引起软件错误的重要来源。需求规格说明是需求分析阶段的产品，我们通常采用的是未使用任何限制非形式化的自然语言进行描述，这种自然语言书写的需求说明，虽然易于理解和使用，但难以保证其正确性、完整性、无二义性、一致性，验证过程只能采用不太规范、不太严格的人工走查的方法进行检查，稍微复杂一些软件的需求规格说明的检查，实际上已经超出了人工检查的能力。 作为软件工程一个重要分支的需求工程，是指应用已证实有效的技术、方法进行需求分析，确定客户需求，帮助分析人员理解问题并定义目标系统的所有外部特征的一门学科。需求规格的获取、表示以及验证是需求工程研究的核心。 本文的主旨是关于需求分析建模和模型验证技术的研究，文中的“分析模型”是需求规格说明的半形式化表示。本文较为全面地研究了以结构化和面向对象两大主流分析方法为基础的需求分析建模技术，包括两种分析方法发展的简史和主要思想，以及基于两种方法的分析模型的构成。并讨论了模型验证的内容、两种方式：静态验证和动态验证的实现原理。根据我国航天工业界软件开发水平的现状以及飞行软件的特点，本文选择了一套结构化建模技术，以期成为航天工业界的需求分析说明规范，同时，为了加速规范的推广，研制了一个支持上述建模技术的CASE工具：TSA，本文结合CASE工具在需求分析中的辅助范围和需求分析人员实际需要的辅助功能，分析得到TSA的设计框架，并以设计框架为基础叙述了实现的技术途径。TSA在航天分布式单元（HDU）开发的需求分析阶段经过初步测试性使用，证实了它在辅助分析建模、模型验证上所起的作用基本达到了预期的效果。