需求工程是软件生命周期中极其主要的一个环节.目前,与软件需求相关的方法和文献有几十种之多,且新的方法层出不穷.但由于软件需求自身所固有的模糊性和不确切性,不管采用哪种非形式化的分析、规约和验证技术,软件需求的完整性、一致性、正确性、可靠性等都难以得到有效的保证.另外,由于软件需求所固有的抽象性,无法像程序代码一样进行直接的测试,导致软件需求的质量始终无法有质的突破,形成了所谓的质量顶峰(qualityceiling)[2].与此同时,软件在系统中的作用越来越重要,软件自身也越来越复杂,特别对于航天、医疗等领域的软件系统,更要求有可证明的软件质量保证.为此,学术界和工业界又先后开发了多种形式化的软件需求方法与技术,以期具有严格数学基础的形式化技术能补充现有的如走查、审查、复审等非形式化的需求质量保证技术,从实质上提高软件需求的质量,降低软件修正和维护的费用. 本文首先概述软件需求形式化方法，接着对各种软件需求形式化进行了分类和比较，然后通过一个实例介绍了两种典型的软件需求形式化方法，最后讨论软件需求形式化的优缺点并总结全文。