题目：Event-B在嵌入式系统建模中的应用研究

随着软硬件相结合的嵌入式系统的应用领域越来越广泛，对其可靠性及安全性要求也越来越高。形式化方法为人们提供了一条思路，来保证系统是构造即正确的。然而，一般的形式化方法仅从软件角度来进行描述，并不能很好地支持对软硬件一同建模，因而也就可能忽略了这种软硬件间的交互。Event-B作为一种系统级的形式化建模方法，支持基于精化的开发过程，并且能够验证不同精化级别之间的一致性，目前，具有Rodin平台的支持，在系统级应用方面表现出更大的潜力。然而，国内缺乏相关的应用研究。本论文基于Event-B这种新的形式化方法结合具体的系统展开研究。本文分析总结了国内外在相关领域的研究状况，首先，对Event-B的组件和数学基础进行了总结，其次，阐述了基于Event-B的建模流程，对流程中的需求预处理方法，精化方法，证明义务生成规则进行了细致的说明，同时，从模型复用的角度总结了四种对控制系统特定行为建模的方法。然后，本文选取起落架收放控制系统作为应用对象进行研究，结合流程及相关方法指导该系统的建模，通过精化逐步得到完善的系统模型，完成的模型能够有序的完成起落架的收放控制。通过建模过程，不仅对系统有了更深入的了解，还可以发现一些遗漏的需求及需求中的不一致。最后，结合建模应用，提出了一种基于Event-B的系统安全性验证方法，为今后进行系统安全性验证和安全关键系统的开发提供了思路。