{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:22:54Z","timestamp":1750220574514,"version":"3.41.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319572871"},{"type":"electronic","value":"9783319572888"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_24","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T06:45:05Z","timestamp":1491633905000},"page":"327-341","source":"Crossref","is-referenced-by-count":5,"title":["Event-B at Work: Some Lessons Learnt from an Application to a Robot Anti-collision Function"],"prefix":"10.1007","author":[{"given":"Arnaud","family":"Dieumegard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ning","family":"Ge","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Jenn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,9]]},"reference":[{"key":"24_CR1","unstructured":"Cuenot, P., Jenn, E., Faure, E., Broueilh, N., Rouland, E.: An experiment on exploiting virtual platforms for the development of embedded equipments. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016) (2016)"},{"key":"24_CR2","unstructured":"SAE: SAE ARP4754 Certification Considerations for Highly-Integrated Or Complex Aircraft Systems. Society of Automotive Engineers (SAE), Warrendale, USA (1996)"},{"key":"24_CR3","unstructured":"RTCA: DO-178C, Software Considerations in Airborne Systems and Equipment Certification. Special Committee 205 of RTCA (2011)"},{"key":"24_CR4","unstructured":"RTCA: DO-333 Formal Methods Supplement to DO-178C and DO-278A. RTCA & EUROCAE, December 2011"},{"key":"24_CR5","unstructured":"RTCA: DO-331 Model-Based Development and Verification Supplement to DO-178C and DO-278A. RTCA & EUROCAE, December 2011"},{"key":"24_CR6","unstructured":"Ge, N., Dieumegard, A., Jenn, E., Voisin, L.: From Event-B to verified C via HLL, October 2016"},{"key":"24_CR7","unstructured":"Clabaut, M., Ge, N., Breton, N., Jenn, E., Delmas, R., Fonteneau, Y.: Industrial grade model checking use cases, constraints, tools and applications. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Toulouse, France (2016)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-319-45943-1_12","volume-title":"Critical Systems: Formal Methods and Automated Verification","author":"N Ge","year":"2016","unstructured":"Ge, N., Jenn, E., Breton, N., Fonteneau, Y.: Formal verification of a rover anti-collision system. In: Beek, Maurice H., Gnesi, S., Knapp, A. (eds.) FMICS\/AVoCS -2016. LNCS, vol. 9933, pp. 171\u2013188. Springer, Cham (2016). doi: 10.1007\/978-3-319-45943-1_12"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Singh, N.K., Ait-Ameur, Y., Pantel, M., Dieumegard, A., Jenn, E.: Stepwise formal modeling and verification of self-adaptive systems with Event-B. The automatic rover protection case study. Presented at the ICECCS 2016 (2016)","DOI":"10.1109\/ICECCS.2016.015"},{"key":"24_CR10","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B - System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"24_CR11","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"24_CR12","volume-title":"Formal Methods Applied to Complex Systems: Implementation of the B Method","author":"J-L Boulanger","year":"2014","unstructured":"Boulanger, J.-L.: Formal Methods Applied to Complex Systems: Implementation of the B Method. Wiley, Hoboken (2014)"},{"key":"24_CR13","unstructured":"Butler, M.: Towards a cookbook for modelling and refinement of control problems (2009)"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-642-24559-6_30","volume-title":"Formal Methods and Software Engineering","author":"W Su","year":"2011","unstructured":"Su, W., Abrial, J.-R., Huang, R., Zhu, H.: From requirements to development: methodology and example. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 437\u2013455. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24559-6_30"},{"key":"24_CR15","unstructured":"Mashkoor, A., Jacquot, J.-P., Souqui\u00e8res, J.: Transformation heuristics for formal requirements validation by animation. In: 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems-SafeCert 2009 (2009)"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-11811-1_22","volume-title":"Abstract State Machines, Alloy, B and Z","author":"S Hallerstede","year":"2010","unstructured":"Hallerstede, S., Leuschel, M., Plagge, D.: Refinement-animation for Event-B \u2014 towards a method of validation. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 287\u2013301. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11811-1_22"},{"key":"24_CR17","unstructured":"Savicks, V., Butler, M., Colley, J., Bendisposto, J.: Rodin multi-simulation plug-in. Presented at the 5th Rodin User and Developer Workshop, Toulouse, France (2014)"},{"key":"24_CR18","unstructured":"Yang, F.: A simulation framework for the validation of Event-B specifications. Universit\u00e9 de Lorraine (2013)"},{"key":"24_CR19","unstructured":"Singh, N.K.: Reliability and safety of critical device software systems. Ecole Centrale de Nantes (2011)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45236-2_46"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-04570-7_17","volume-title":"Formal Methods for Industrial Critical Systems","author":"L Ladenberger","year":"2009","unstructured":"Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202\u2013204. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04570-7_17"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Yang, F., Jacquot, J.-P., Souqui\u00e8res, J.: JeB: safe simulation of Event-B models in Javascript. In: 2013 20th Asia-Pacific Software Engineering Conference (APSEC), vol. 1, pp. 571\u2013576 (2013)","DOI":"10.1109\/APSEC.2013.83"},{"key":"24_CR23","unstructured":"MIRA Ltd: MISRA-C:2004 guidelines for the use of the C language in critical systems (2004)"},{"key":"24_CR24","unstructured":"Petre, L., Sere, K., Tsiopoulos, L.: Deploy methods: final report. D44, April 2012"},{"issue":"1","key":"24_CR25","doi-asserted-by":"crossref","first-page":"15:1","DOI":"10.1145\/2406336.2406351","volume":"12","author":"D M\u00e9ry","year":"2013","unstructured":"M\u00e9ry, D., Singh, N.K.: Formal specification of medical systems by proof-based refinement. ACM Trans. Embed. Comput. Syst. 12(1), 15:1\u201315:25 (2013)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"24_CR26","first-page":"49","volume-title":"Complex Systems Design & Management 2010","author":"D M\u00e9ry","year":"2010","unstructured":"M\u00e9ry, D., Singh, N.K.: Real-time animation for formal specification. In: M\u00e9ry, D., Singh, N.K. (eds.) Complex Systems Design & Management 2010, pp. 49\u201360. Springer, Heidelberg (2010)"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-16561-0_31","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"D M\u00e9ry","year":"2010","unstructured":"M\u00e9ry, D., Singh, N.K.: Trustable formal specification for software certification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 312\u2013326. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16561-0_31"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems - (QEST 2006), pp. 125\u2013126 (2006)","DOI":"10.1109\/QEST.2006.59"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:30:46Z","timestamp":1750195846000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}