Abstract
We propose a method to build critical embedded control systems in a systematic way. The method covers the modelling of both the digital part and the physical environment of a considered system, and their refinement until more concrete levels. It is based on Event-B in order to benefit from its materials, stepwise refinements and tools. Two main processes are distinguished: one to capture the global model, the other to detail the global model; they are made of several refinement steps which are accompanied with guidelines. The precise description of the interface between the digital and physical parts is used to start the modelling process. The recurrent categories of variables and events in control systems are described and used as guidelines to conduct a systematic construction. We illustrate the method with the landing gear system case study.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundam. Inform. 77(1–2), 1–28 (2007)
Back, R.-J.: Software construction by stepwise feature introduction. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 162–183. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45648-1_9
Banach, R.: The landing gear case study in hybrid Event-B. In: Boniol et al. [6], pp. 126–141 (2014). https://doi.org/10.1007/978-3-319-07512-9_9
Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol et al. [6], pp. 1–18 (2014). https://doi.org/10.1007/978-3-319-07512-9_1
Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.): ABZ 2014. CCIS, vol. 433. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07512-9
Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00255-7_2
Cansell, D., Méry, D.: Playing with abstraction and refinement for managing features interactions. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) ZB 2000. LNCS, vol. 1878, pp. 148–167. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44525-0_10
Damchoom, K., Butler, M.: Applying event and machine decomposition to a flash-based filestore in Event-B. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol. 5902, pp. 134–152. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10452-7_10
Damchoom, K., Butler, M., Abrial, J.-R.: Modelling and proof of a tree-structured file system in Event-B and rodin. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 25–44. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88194-0_5
Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems - A Cyber-Physical Systems Approach. MIT Press, Cambridge (2017)
Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using prob. In: Boniol et al. [6], pp. 66–79 (2014)
Hudon, S., Hoang, T.S.: Development of control systems guided by models of their environment. Electron. Notes Theor. Comput. Sci. 280, 57–68 (2011)
Dragomir, I., Ober, I., Lesens, D.: A case study in formal system engineering with SysML. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, pp. 189–198 (2012)
Jard, C., Roux, O.H. (eds.): Communicating Embedded Systems: Software and Design. Wiley-ISTE (2009)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. In: Boniol et al. [6], pp. 80–94 (2014). https://doi.org/10.1007/978-3-319-07512-9_6
Patcas, L.M., Lawford, M., Maibaum, T.: From system requirements to software requirements in the four-variable model. ECEASST 66 (2013). http://journal.ub.tu-berlin.de/eceasst/article/view/887
Silva, R., Butler, M.: Shared event composition/decomposition in Event-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 122–141. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_7
Su, W., Abrial, J.R.: Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system. In: Boniol et al. [6], pp. 19–35 (2014). https://doi.org/10.1007/978-3-319-07512-9_2
Su, W., Abrial, J.-R., Zhu, H.: Complementary methodologies for developing hybrid systems with Event-B. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 230–248. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34281-3_18
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
André, P., Attiogbé, C., Lanoix, A. (2018). Systematic Construction of Critical Embedded Systems Using Event-B. In: Abdelwahed, E., et al. New Trends in Model and Data Engineering. MEDI 2018. Communications in Computer and Information Science, vol 929. Springer, Cham. https://doi.org/10.1007/978-3-030-02852-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-030-02852-7_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02851-0
Online ISBN: 978-3-030-02852-7
eBook Packages: Computer ScienceComputer Science (R0)