J. Abrial, Modeling in Event-B: System and Software Engineering, 2010.
DOI : 10.1017/CBO9781139195881

R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

R. J. Back, On correct refinement of programs, Journal of Computer and System Sciences, vol.23, issue.1, pp.49-68, 1981.
DOI : 10.1016/0022-0000(81)90005-2

D. Bjørner and M. C. Henson, Logics of Specification Languages, EATCS Textbook in Computer Science, 2007.
DOI : 10.1007/978-3-540-74107-7

F. Boniol and V. Wiels, Landing Gear System, 2013.

R. W. Butler and G. B. Finelli, The infeasibility of quantifying the reliability of life-critical real-time software. Software Engineering, IEEE Transactions on, vol.19, issue.1, pp.3-12, 1993.

D. Cansell and D. Méry, The event-B Modelling Method: Concepts and Case Studies, pp.33-140, 2007.
DOI : 10.1007/978-3-540-74107-7_3
URL : https://hal.archives-ouvertes.fr/inria-00579550

D. Cansell, D. Méry, and J. Rehm, Time Constraint Patterns for Event B Development, Lecture Notes in Computer Science, vol.4355, pp.140-154, 2006.
DOI : 10.1007/11955757_13
URL : https://hal.archives-ouvertes.fr/hal-00149163

E. Gamma, R. Helm, R. Johnson, R. Vlissides, and P. Gamma, Design Patterns : Elements of Reusable Object-Oriented Software design Patterns, 1994.

C. Sally, R. W. Johnson, and . Butler, Formal Methods, Chapter 21 in The Avionics Handbook, 2001.

T. Gary, J. Leavens, D. Abrial, M. Batory, A. Butler et al., Roadmap for enhanced languages and methods to aid verification, Fifth Intl. Conf. Generative Programming and Component Engineering, pp.221-235, 2006.

M. Leuschel and M. Butler, ProB: A Model Checker for B, Lecture Notes in Computer Science, pp.855-874, 2003.
DOI : 10.1007/978-3-540-45236-2_46

D. Méry and N. Singh, Modelling an aircraft landing system in event-b, ABZ Case Study, 2014.

. Neeraj-kumar and . Singh, × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act27 : open EV := F ALSE act28 : gears locked down := T RU E act29 : gears man := F ALSE act30 : anomaly := F ALSE act31 : general EV f unc :? (1 .. 3 ? P OSIT ION S) × (1 .. 3 ? A Switch), Using Event-B for Critical Device Software Systems. Springer-Verlag GmbH, 2013. (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act32)) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act35 : open EV f unc :? (1 .. 3 ? P OSIT ION S) × (1 .. 3 ? A Switch) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? (GEARS ? BOOL)))) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act33 : retract EV f unc :? (1 .. 3 ? P OSIT ION S) × (1 .. 3 ? A Switch) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act34 : extend EV f unc :? (1 .. 3 ? P OSIT ION S) × (1 .. 3 ? A Switch) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act35 : open EV f unc :? (1 .. 3 ? P OSIT ION S) × (1 .. 3 ? A Switch) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act36 : gears locked down f unc :? (1 .. 3 ? P OSIT ION S) × (1 .. 3 ? A Switch) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act37 : gears man f unc :? (1 .. 3 ? P OSIT ION S) × (1 .. 3 ? A Switch) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL act38 : anomaly f unc :? (1 .. 3 ? P OSIT ION S) × (1 .. 3 ? A Switch) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? (GEARS ? BOOL)) × (1 .. 3 ? GEAR ABSORBER) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? (DOORS ? BOOL)) × (1 .. 3 ? BOOL) ? BOOL