需求工程出现于上个世纪80年代中期，目前已发展成为软件工程的一个独立研究分支。需求获取技术是需求工程中一个非常重要的研究内容。如何用适当的方法把软件需求详细精确地描述出来，这不仅影响着开发人员之间对软件系统的理解和的交流，更影响到最终软件产品的成败，尤其是安全悠关系统的开发中。
　　目前主流的软件需求描述方法有两类：自然语言描述和半形式化描述，自然语言描述是目前工程实践中使用的主要方法，半形式化描述以UML/OCL为代表。自然语言存在着二义性和不一致性等缺陷，而UML/OCL的建模元素同样缺乏精确的形式化语义，也不可避免地产生多义性，尽管辅之以OCL可以在一定程度上减少歧义性，但仍不能从根本上解决UML需求模型歧义性的问题。以这两类方法为基础的软件需求描述和构造过程往往潜藏着大量的错误和缺陷，错误在一定程度上可以依靠测试来解决，软件需求中的缺陷，测试是无能为力的。形式化方法作为一种以数学为基础的方法，能够清晰、精确、抽象、简明地描述和验证软件系统及其性质，能够发现软件需求中的缺陷，极大地提高软件的安全性和可靠性，但在需求获取过程中尚无形式化方法成功应用的案例。
　　基于此，本文提出了一种形式化的需求获取方法，首先在离散系统模型的基础上，提出了一个可以适用于软件生命周期所有阶段的模型－公平离散系统模型，并给出了其在软件需求获取过程中求精、验证和控制复杂性的方法、需求模型复用的概念。接下来，采用Event-B完整地描述形式化的需求获取的全过程,对Event-B的模型结构进行了扩充，把从规约到程序求精和验证的概念延伸到需求获取过程中，并详细地解释了需求获取过程中需求求精验证和从规约到程序求精验证的本质区别。在需求模型复杂性控制方法上，给出了模型分解的新算法，求精过程中给出事件引入的新策略，同时详细给出了需求模型复用的策略。相应的，以景区管理系统中的门禁子系统需求模型获取为例，详细地说明了本方法在实际工程中的应用。因Event-B仅考虑了MP公平性下活性的描述和验证规则，在最后在相关工作的基础上做了部分的进一步工作。