{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:53:29Z","timestamp":1740099209978,"version":"3.37.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030028510"},{"type":"electronic","value":"9783030028527"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02852-7_18","type":"book-chapter","created":{"date-parts":[[2018,10,17]],"date-time":"2018-10-17T17:41:45Z","timestamp":1539798105000},"page":"200-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Systematic Construction of Critical Embedded Systems Using Event-B"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Andr\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Attiogb\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Lanoix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,18]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B - System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"1\u20132","key":"18_CR2","first-page":"1","volume":"77","author":"JR Abrial","year":"2007","unstructured":"Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundam. Inform. 77(1\u20132), 1\u201328 (2007)","journal-title":"Fundam. Inform."},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-45648-1_9","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"R-J Back","year":"2002","unstructured":"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\u2013183. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45648-1_9"},{"key":"18_CR4","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-07512-9_9","volume-title":"Communications in Computer and Information Science","author":"Richard Banach","year":"2014","unstructured":"Banach, R.: The landing gear case study in hybrid Event-B. In: Boniol et al. [6], pp. 126\u2013141 (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_9"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-07512-9_1","volume-title":"Communications in Computer and Information Science","author":"Fr\u00e9d\u00e9ric Boniol","year":"2014","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol et al. [6], pp. 1\u201318 (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_1"},{"key":"18_CR6","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07512-9","volume-title":"ABZ 2014: The Landing Gear Case Study","year":"2014","unstructured":"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"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-00255-7_2","volume-title":"Integrated Formal Methods","author":"M Butler","year":"2009","unstructured":"Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20\u201338. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00255-7_2"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-44525-0_10","volume-title":"ZB 2000: Formal Specification and Development in Z and B","author":"D Cansell","year":"2000","unstructured":"Cansell, D., M\u00e9ry, 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\u2013167. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44525-0_10"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-10452-7_10","volume-title":"Formal Methods: Foundations and Applications","author":"K Damchoom","year":"2009","unstructured":"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\u2013152. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10452-7_10"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-88194-0_5","volume-title":"Formal Methods and Software Engineering","author":"K Damchoom","year":"2008","unstructured":"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\u201344. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88194-0_5"},{"key":"18_CR11","volume-title":"Introduction to Embedded Systems - A Cyber-Physical Systems Approach","author":"EA Lee","year":"2017","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems - A Cyber-Physical Systems Approach. MIT Press, Cambridge (2017)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"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\u201379 (2014)","DOI":"10.1007\/978-3-319-07512-9_5"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.entcs.2011.11.018","volume":"280","author":"S Hudon","year":"2011","unstructured":"Hudon, S., Hoang, T.S.: Development of control systems guided by models of their environment. Electron. Notes Theor. Comput. Sci. 280, 57\u201368 (2011)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013198 (2012)","DOI":"10.1109\/ICECCS20050.2012.6299214"},{"key":"18_CR15","unstructured":"Jard, C., Roux, O.H. (eds.): Communicating Embedded Systems: Software and Design. Wiley-ISTE (2009)"},{"issue":"7","key":"18_CR16","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-319-07512-9_6","volume-title":"Communications in Computer and Information Science","author":"Amel Mammar","year":"2014","unstructured":"Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. In: Boniol et al. [6], pp. 80\u201394 (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_6"},{"key":"18_CR18","unstructured":"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"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-25271-6_7","volume-title":"Formal Methods for Components and Objects","author":"R Silva","year":"2011","unstructured":"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\u2013141. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_7"},{"key":"18_CR20","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-07512-9_2","volume-title":"Communications in Computer and Information Science","author":"Wen Su","year":"2014","unstructured":"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\u201335 (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_2"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-34281-3_18","volume-title":"Formal Methods and Software Engineering","author":"W Su","year":"2012","unstructured":"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\u2013248. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34281-3_18"}],"container-title":["Communications in Computer and Information Science","New Trends in Model and Data Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02852-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T09:19:56Z","timestamp":1605259196000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02852-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030028510","9783030028527"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02852-7_18","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"MEDI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Model and Data Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"medi2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/medi2018.uca.ma\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}