Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system

Rodin development for this Paper. http://www.cas.mcmaster.ca/~khedri/?page_id=778

Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)

Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)

Abrial, J.-R., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, Farhad, Voisin, Laurent: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010)

Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Proceedings of B’98: Recent Advances in the Development and Use of the B Method, 2nd International B Conference, Montpellier, 22–24 April 1998, pp. 83–128 (1998)

Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: ABZ, pp. 178–193 (2012)

Anim, B. http://www.animb.org

Atelier, B.: http://www.atelierb.eu

Barrett, C.W., de Moura, L., Stump, A.: Smt-comp: satisfiability modulo theories competition. In: Proceedings of 17th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 357, Edinburgh, Scotland, 6–10 July 2005

Boniol, F., Wiels, V.: The Landing Gear System Case Study. In: ABZ Case Study. Communications in Computer Information Science, vol. 433. Springer (2014)

Boström, P.: Creating sequential programs from Event-B models. In: Proceedings of, 8th International Conference on Integrated Formal Methods, pp. 74–88. Nancy, 11–14 Oct 2010

Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient satisfiability modulo theories via delayed theory combination. In: Proceedings of the 17th International Conference on Computer Aided Verification, pp. 335–349 (2005)

Cansell, D., Méry, D., Rehm, J.: Time constraint patterns for Event-B development. In: Proceedings of B 2007: Formal Specification and Development in B, 7th International Conference of B Users, pp. 140–154. Besançon, 17–19 January 2007

Peter, F., Vadim, E.: Modelica—a unified object-oriented language for system modelling and simulation. In Proceedings of ECOOP’98—Object-Oriented Programming, 12th European Conference, pp. 67–90. Brussels, 20-24 July 1998

Fürst A., Hoang, T.S., Basin, D.A., Desai, K., Sato, N., Miyazaki, K.: Code generation for Event-B. In: Proceedings of 11th International Conference on Integrated Formal Methods, pp. 323–338. Bertinoro, 9–11 Sept 2014

Hallerstede, S., Jastram, M., Ladenberger, L.: A method and tool for tracing requirements into specifications. Science of Computer Programming, p. 36 (2013)

Hallerstede, S., Jastram, M., Ladenberger, L.: A method and tool for tracing requirements into specifications. Sci. Comput. Program. 82, 2–21 (2014)

Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP 11(4–5), 767–782 (2011)

Hoang, T.S., Abrial, J.-R.: Reasoning about liveness properties in Event-B. In: Proceedings of 13th International Conference on Formal Engineering Methods on Formal Methods and Software Engineering, pp. 456–471. Durham, 26–28 Oct 2011

Hoang, T.S., Fürst, A., Abrial, J.-R.: Event-B patterns and their tool support. Softw. Syst. Model. 12(2), 229–244 (2013)

Kuruma, H., Basin, D.A., Abrial, J.-R.: Developing topology discovery in Event-B. Sci. Comput. Program. 74(11–12), 879–899 (2009)

Hudon, S., Hoang, T.S.: Development of control systems guided by models of their environment. Electron. Notes Theor. Comput. Sci. 280, 57–68 (2011)

Larman, C.: Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and Iterative Development. Prentice Hall, Upper Saddle River (2004)

Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)

Manna, Z., Pnueli, A.: Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comput. Program. 4(3), 257–289 (1984)

Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems Specification. Springer, New York (1992)

Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems Safety. Springer, New York (1995)

MathWorks. http://www.mathworks.com/

Méry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings of the 2011 Symposium on Information and Communication Technology, Hanoi, pp. 179–188. 13–14 Oct 2011

Otter, M., Malmheden, M., Elmqvist, H., Mattsson, S.E., Johnsson, C.: A new formalism for modeling of reactive and hybrid systems. In: 7th international Modelica Conference, pp. 364–377 (2009)

Rodin. http://www.event-b.org/

Said, M.Y., Butler, M.J., Snook, C.F.: Language and tool support for class and state machine refinement in UML-B. In: Proceedings of Formal Methods, Second World Congress, Eindhoven, pp. 579–595. 2–6 Nov 2009

Sarshogh, M.R., Butler, M.J.: Specification and refinement of discrete timing properties in Event-B. ECEASST, vol. 46 (2011)

Savicks, V., Butler, M., Colley, J.: Co-simulation environment for Rodin: landing gear case study. In: ABZ 2014: The Landing Gear Case Study, pp. 148–153 (2014)

Wen, S., Abrial J.-R., Runlei, H., Huibiao, Z.: From requirements to development: Methodology and example. In: ICFEM, pp. 437–455 (2011)

Su W., Abrial J.-R., Zhu H.: Complementary methodologies for developing hybrid systems with Event-B. In: ICFEM, pp. 230–248 (2012)

Voisin, L., Abrial, J.-R.: The rodin platform has turned ten. In: Proceedings of Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, pp. 1–8. Toulouse, 2–6 June 2014

Yeganefard, S., Butler, M.J., Rezazadeh, A.: Evaluation of a guideline by formal modelling of cruise control system in Event-B. In: Proceedings of Second NASA Formal Methods Symposium—NFM 2010, pp. 182–191. Washington D.C., 13–15 April 2010