起落架系统的建模与分析:一种基于 Event-B/Rodin 的解决方案
软件工程
2018-03-16 v1
摘要
本文给出使用 Event-B 与 Rodin 对起落架系统案例研究的解决方案。我们研究整个系统(包括数字部分与被控部分)。我们利用特征扩充构建整个系统的抽象模型,并利用结构精化更具体地细化数字部分。所需的安全性质被形式化并证明。我们提出一种处理一类可达性性质的具体方法。研究期间进行的实验由 Rodin 工具支持。我们表明所提方案具有系统性,可应用于类似案例研究。
引用
@article{arxiv.1803.05647,
title = {Modelling and Analysing the Landing Gear System: a Solution with Event-B/Rodin},
author = {Pascal André and Christian Attiogbé and Arnaud Lanoix},
journal= {arXiv preprint arXiv:1803.05647},
year = {2018}
}