Abstract Aircrafts are the safest means of transport, which requires an excellent management and development. Whereas, Aircraft landing is one of the most complex problems in this domain, Due to the huge increase of aircrafts number in the world. One of the main challenges to develop landing system is specifying it in the first place. In this paper, we focus on modeling aircrafts scheduling in the Traffic Management Advisor, our approach is based on deadline monotonic algorithm that shows a lot of advantages compared to the currently used method -First come First Served-. To ensure a very strong assurance of bug’s absence, we model this system using a formal method -Event-B- prove that it is correct by construction. This modeling is done by mean of refinement, invariants preservation proof and deadlock freedom, whereby the result system, will be correct by construction. However, the number of proofs that ensure system correctness is huge, therefore we use a platform called RODIN to minimize the number of proofs done manually.
Modeling Aircraft Landing Scheduling in Event B
2017-12-02
16 pages
Article/Chapter (Book)
Electronic Resource
English
Modeling an Aircraft Landing System in Event-B
British Library Conference Proceedings | 2014
|Modeling an Aircraft Landing System in Event-B
Springer Verlag | 2014
|Mobile Aircraft Landing Stair Scheduling
IEEE | 2019
|