在当今社会中,社会信息化高速发展,每一个行业都与软件紧密相关。在开发一个软件时,首先要做的是对软件需求进行分析,而在这个分析描述的过程中又避免不了因语法或语义带来的错误。为了减轻这些不必要的错误带来的损失,形式化方法应运而生。目前形式化方法领域中,比较常见的两种方法是B方法和Event-B方法,Event-B方法由B方法演化而来,具有许多B方法没有的优点,并且Event-B方法在工具平台上有着很大的优势。Rodin平台是基于Eclipse开发的集成环境,为Event-B方法提供了系统级的开发模式,可以通过逐层精化的方式为模型添加所需的属性和功能,并且Rodin平台简化了 Event-B方法的验证过程,提供了多种自动证明器,支持更多的证明义务,为模型的精化和证明提供了有效的支持,同时最小化对更改现有证明的影响,在软件开发的前期就保证了软件模型的正确性和一致性。本文以免疫系统作为开发需求,使用Event-B方法建立免疫系统抽象模型,并详细阐述在Rodin平台下对该模型从需求分析到验证的全部过程,主要开展了如下工作:(1)研究了现阶段常用的形式化方法B方法与Event-B方法各自的建模方式,介绍了 B方法的开发过程和优缺点,并在此基础之上针对免疫系统的需求对两种方法作出比较,特别是精化方式和交互式证明方面,阐述选择Event-B方法进行免疫系统建模的原因。(2)研究以免疫系统为例的Event-B形式化方法的建模过程,创建免疫系统初代抽象模型,然后通过逐步精化的方式向模型中添加属性和功能,使系统更加完善,直至满足所有的需求。(3)研究在Rodin平台上的抽象模型验证方式,介绍了几类自动证明器和免疫系统抽象模型证明中所使用到的证明义务,并联系免疫模型进行了推理演示。最后,通过交互式证明的方式完成整个免疫模型的证明。总的来说,Event-B形式化方法能够很好的帮助开发人员完成对软件系统需求准确性和一致性的验证。本文通过建立基于Event-B方法的免疫系统抽象模型,详细地展示了从需求重写到模型验证的全过程,体现了在软件开发前期使用形式化进行模型验证的重要性。