软件工程中的需求分析是指通过对要解决的问题的分析与理解,为问题涉及的信息、功能及系统行为建立模型,将用户需求精确化、完全化,最终形成需求规约说明。而用于需求分析的形式化方法是以严格的数学理论为基础,用数学的方法来帮助需求分析人员解决目标系统系统“做什么”的问题。模态迁移系统是一种基于状态机的形式化建模方法,普遍应用于对系统行为的形式规约。该方法通常假定在某种层次上,已经完整描述目标系统的行为。尽管这一假设对已经完全探知其属性的命题来说是有效的,但在系统行为建模的初期是不能满足需求的,系统需求的捕获过程中需求信息是逐步完善的。为获取目标系统更正确完整的需求规约,本文通过扩展模态迁移系统,定义了局部模态迁移系统来更精确的描述目标系统的局部行为。局部模态迁移系统对用户需求描述中的必然行为、不确定行为和禁止行为,都给出了相应的形式规约说明。在局部模态迁移系统中未描述的行为被认为超出了特定用户关注的范围,是与之无关的未定义行为。为消除局部行为模型中存在的不确定行为,获取目标系统的全局行为模型,文中提出了一种基于事件和状态的局部行为模型合并方法。该方法首先定义了模型之间的精化关系,利用精化关系比较谁是目标系统更“确定的”的模型,这也就为确定什么样的模型是我们期望的合并模型提供了依据。由于我们通常希望合并模型不增加额外的需求信息,因此其合并过程就是构建初始模型的最小共同精化(或极小共同精化)的过程。通过文中定义的+u操作符和+1操作符可以分别确定合并模型的上界与最大下界。建模者可以选择性的对最大下界进一步精化获得预期的极小共同精化。通过对目标系统所有局部行为模型的合并,以及在合并过程中不断的与相关用户交互,可以精化模型中存在的不确定行为,逐步捕获目标系统的所有必然行为。最终的全局行为模型应该只包含有必然迁移和禁止迁移,这样也就得到了我们所期望的初始模型的实现：局部标号迁移系统模型。