{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,10]],"date-time":"2025-05-10T20:04:05Z","timestamp":1746907445189,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319478456"},{"type":"electronic","value":"9783319478463"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47846-3_8","type":"book-chapter","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T02:53:57Z","timestamp":1476413637000},"page":"106-121","source":"Crossref","is-referenced-by-count":8,"title":["A System Substitution Mechanism for Hybrid Systems in Event-B"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Babin","sequence":"first","affiliation":[]},{"given":"Yamine","family":"A\u00eft-Ameur","sequence":"additional","affiliation":[]},{"given":"Neeraj Kumar","family":"Singh","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Pantel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,15]]},"reference":[{"key":"8_CR1","unstructured":"Models. http:\/\/babin.perso.enseeiht.fr\/r\/ICFEM_2016_Models\/"},{"key":"8_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996). http:\/\/ebooks.cambridge.org\/ebook.jsf?bid=CBO9780511624162"},{"key":"8_CR3","doi-asserted-by":"crossref","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, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"issue":"6","key":"8_CR4","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hong, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR5","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Leuschel, M., Schmalz, M., Voisin, L.: Proposals for mathematical extensions for Event-B. Technical report (2009)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-25942-0_4","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"G Babin","year":"2015","unstructured":"Babin, G., A\u00eft-Ameur, Y., Nakajima, S., Pantel, M.: Refinement and proof based development of\u00a0systems characterized by continuous functions. In: Li, X., et al. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 55\u201370. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-25942-0_4"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Babin, G., A\u00eft-Ameur, Y., Pantel, M.: Formal verification of runtime compensation of web service compositions: a refinement and proof based proposal with Event-B. In: IEEE International Conference on Services Computing, pp. 98\u2013105 (2015)","DOI":"10.1109\/SCC.2015.23"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Babin, G., A\u00eft-Ameur, Y., Pantel, M.: Correct instantiation of a system reconfiguration pattern: a proof and refinement-based approach. In: IEEE International Symposium on High Assurance Systems Engineering (HASE), pp. 31\u201338 (2016)","DOI":"10.1109\/HASE.2016.47"},{"key":"8_CR9","volume-title":"A Generic Model for System Substitution","author":"G Babin","year":"2016","unstructured":"Babin, G., A\u00eft-Ameur, Y., Pantel, M.: Trustworthy cyber-physical systems engineering. In: Romanovsky, A., Ishikawa, F. (eds.) A Generic Model for System Substitution. Chapman and Hall\/CRC, Boca Raton (2016)"},{"key":"8_CR10","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1016\/j.scico.2015.02.003","volume":"105","author":"R Banach","year":"2015","unstructured":"Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core hybrid Event-B I: single hybrid Event-B machines. Sci. Comput. Program. 105, 92\u2013123 (2015)","journal-title":"Sci. Comput. Program."},{"key":"8_CR11","unstructured":"Bhattacharyya, A.: Formal modelling and analysis of dynamic reconfiguration of dependable systems. Ph.D. thesis, Newcastle University, January 2013"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Butler, M., Abrial, J.R., Banach, R.: From Action Systems to Distributed Systems: The Refinement Approach, chap. Modelling and Refining Hybrid Systems in Event-B and Rodin, pp. 29\u201342. Chapman and Hall\/CRC., April 2016","DOI":"10.1201\/b20053-5"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-3-642-39698-4_5","volume-title":"Theories of Programming and Formal Methods","author":"M Butler","year":"2013","unstructured":"Butler, M., Maamria, I.: Practical theory extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67\u201381. Springer, Heidelberg (2013)"},{"issue":"1\u20132","key":"8_CR14","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 110\u2013122 (1997). http:\/\/dx.doi.org\/10.1007\/s100090050008","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Iftikhar, M.U., Weyns, D.: A case study on formal verification of self-adaptive behaviors in a decentralized system. In: Kokash, N., Ravara, A. (eds.) 11th International Workshop on Foundations of Coordination Languages and Self Adaptation (FOCLASA 2012), EPTCS, vol. 91, pp. 45\u201362 (2012)","DOI":"10.4204\/EPTCS.91.4"},{"key":"8_CR16","volume-title":"Rodin User\u2019s Handbook: Covers Rodin V.2.8","author":"M Jastram","year":"2014","unstructured":"Jastram, M., Butler, M.: Rodin User\u2019s Handbook: Covers Rodin V.2.8. CreateSpace Independent Publishing Platform, USA (2014). ISBN 10: 1495438147, ISBN 13: 9781495438141, http:\/\/handbook.event-b.org"},{"issue":"2","key":"8_CR17","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.entcs.2011.11.011","volume":"279","author":"A Lanoix","year":"2011","unstructured":"Lanoix, A., Dormoy, J., Kouchnarenko, O.: Combining proof and model-checking to validate reconfigurable architectures. Electron. Notes Theor. Comput. Sci. 279(2), 43\u201357 (2011)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"8_CR18","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems - A Cyber-Physical Systems Approach. LeeSeshia.org, 1.5 edn. (2014). http:\/\/leeseshia.org\/"},{"issue":"02","key":"8_CR19","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1142\/S2301385014300029","volume":"02","author":"H Lin","year":"2014","unstructured":"Lin, H.: Mission accomplished: an introduction to formal methods in mobile robot motion planning and control. Unmanned Syst. 02(02), 201\u2013216 (2014)","journal-title":"Unmanned Syst."},{"issue":"1","key":"8_CR20","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1504\/IJCCBS.2013.053743","volume":"4","author":"I Pereverzeva","year":"2013","unstructured":"Pereverzeva, I., Troubitsyna, E., Laibinis, L.: A refinement-based approach to developing critical multi-agent systems. Int. J. Crit. Comput.-Based Syst. 4(1), 69\u201391 (2013)","journal-title":"Int. J. Crit. Comput.-Based Syst."},{"key":"8_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). http:\/\/symbolaris.com\/lahs\/"},{"issue":"2","key":"8_CR22","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1109\/TDSC.2010.52","volume":"9","author":"R Rodrigues","year":"2012","unstructured":"Rodrigues, R., Liskov, B., Chen, K., Liskov, M., Schultz, D.: Automatic reconfiguration for large-scale reliable storage systems. IEEE Trans. Dependable Secure Comput. 9(2), 145\u2013158 (2012)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"8_CR23","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1016\/j.scico.2014.04.015","volume":"94","author":"W Su","year":"2014","unstructured":"Su, W., Abrial, J.R., Zhu, H.: Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program. 94, 164\u2013202 (2014)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47846-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T11:53:33Z","timestamp":1568462013000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47846-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319478456","9783319478463"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47846-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}