事件B中的飞机着陆系统建模（完整报告）
Modelling an Aircraft Landing System in Event-B (Full Report)
摘要：
关键系统中的硬件或软件故障可能导致生命损失。在系统开发过程中，设计错误可能是引入故障的主要原因。形式化技术是验证关键系统正确性的一种替代方法，克服了传统验证技术如仿真和测试的局限性。日益增加的复杂性和故障率给航空电子系统的验证和确认领域带来了新的挑战。由于软件的可靠性无法量化，因此\textit{correct by construction}方法可以实现可靠的系统。精化在从抽象规范到具体系统的增量式构建大型系统中扮演着重要角色。本文是对某型飞机着陆系统的逐步形式化开发。正式的模型包括复杂的行为，时间行为和起落架系统的操作顺序。模型的形式化事件B建模语言，支持逐步细化。该案例研究被认为是专门用于验证系统行为特性的技术和工具的基准。该报告是为ABZ 2014案例研究发表的论文的完整版本。是
英文摘要：
The failure of hardware or software in a critical system can lead to loss of lives. The design errors can be main source of the failures that can be introduced during system development process. Formal techniques are an alternative approach to verify the correctness of critical systems, overcoming limitations of the traditional validation techniques such as simulation and testing. The increasing complexity and failure rate brings new challenges in the area of verification and validation of avionic systems. Since the reliability of the software cannot be quantified, the \textit{correct by construction} approach can implement a reliable system. Refinement plays a major role to build a large system incrementally from an abstract specification to a concrete system. This paper contributes as a stepwise formal development of the landing system of an aircraft. The formal models include the complex behaviour, temporal behaviour and sequence of operations of the landing gear system. The models are formalized in Event-B modelling language, which supports stepwise refinement. This case study is considered as a benchmark for techniques and tools dedicated to the verification of behavioural properties of systems. The report is the full version of a paper published for the ABZ 2014 Case Study. is
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
