在Event-B中建模飞机着陆系统（完整报告）
软件工程
2014-07-04 v1
摘要
关键系统中硬件或软件的故障可能导致生命损失。设计错误可能是系统开发过程中引入故障的主要来源。形式化技术是验证关键系统正确性的替代方法，克服了传统验证技术（如仿真和测试）的局限性。日益增长的复杂性和故障率给航空电子系统的验证与确认领域带来了新的挑战。由于软件的可靠性无法量化，“正确性通过构造”方法可以实现可靠的系统。精化在从抽象规约逐步构建大型系统到具体系统的过程中起着重要作用。本文贡献了飞机着陆系统的逐步形式化开发。形式化模型包括起落架系统的复杂行为、时间行为和操作序列。模型使用支持逐步精化的Event-B建模语言形式化。该案例研究被视为用于验证系统行为属性的技术和工具的基准。本报告是ABZ 2014案例研究发表论文的完整版本。
引用
@article{arxiv.1407.0927,
title = {Modelling an Aircraft Landing System in Event-B (Full Report)},
author = {Dominique Méry and Neeraj Kumar Singh},
journal= {arXiv preprint arXiv:1407.0927},
year = {2014}
}