使用传统的开发方法对安全关键系统进行开发时,早期系统设计阶段的错误往往到开发后期的测试阶段才能检测出来,重新对系统结构进行错误修改会造成大量的时间和人力耗费。并且由于测试并不能保证系统中不存在错误,无法满足安全关键系统对安全性和可靠性的要求。与之对应的是,形式化开发方法使用精确的数学语言根据系统需求进行描述,消除自然语言带来的二义性,同时,形式化方法根据系统需求进行建模后,使用数学证明的方式来验证模型的正确性,能够在开发早期发现需求与设计上存在的错误,避免了后期的测试所带来的时间和成本消耗。然而,由于形式化方法在使用时需要将自然语言描述的需求文本转换成精确的形式化规约,对开发人员的专业知识背景要求很高。因此一般需要使用需求工程中的需求分析方法将系统需求进行分解,转换成半形式化的中间语言,减轻前期获取需求规约的困难。本文使用SysML/KAOS方法在前期对需求进行处理,将文本需求转换成使用特定标记语言表示的目标(goal)中,然后根据目标模型中的精化分解关系将复杂需求进行分解,建立需求的层次结构。同时,建立从SysML/KAOS方法到形式化建模语言Event-B的关系映射,将目标模型中的目标和需求精化关系转换到Event-B的模型元素中,然后通过Event-B中的验证机制对转换的正确性和一致性进行验证。本文的主要研究工作如下:(1)将SysML/KAOS模型中表示功能需求的实现目标(Achieve goal)和表示安全需求的维持目标(Maintain goal)转换到Event-B模型中的对应元素;(2)将目标模型中的三种需求精化模式对应转换到Event-B的模型精化关系中,同时给出了转换一致性和正确性证明;(3)对于转换中存在的活性属性丢失问题进行讨论,给出了目标模型中活性属性在Event-B建模过程中的表达方式,然后针模型中已经添加的活性属性可能在精化过程中丢失的问题进行研究,给出的精化中活性属性保持的方法和相关证明。