{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T11:39:58Z","timestamp":1725881998482},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319548753"},{"type":"electronic","value":"9783319548760"}],"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-54876-0_3","type":"book-chapter","created":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T04:36:57Z","timestamp":1488343017000},"page":"31-45","source":"Crossref","is-referenced-by-count":3,"title":["A Formal Verification of Safe Update Point Detection in Dynamic Software Updating"],"prefix":"10.1007","author":[{"given":"Razika","family":"Lounas","sequence":"first","affiliation":[]},{"given":"Nisrine","family":"Jafri","sequence":"additional","affiliation":[]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[]},{"given":"Mohamed","family":"Mezghiche","sequence":"additional","affiliation":[]},{"given":"Jean-Louis","family":"Lanet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,2]]},"reference":[{"key":"3_CR1","unstructured":"Baumann, A., Kerr, J., Da Silva, D., Krieger, O., Wisniewski, R.W.: Module hot-swapping for dynamic update and reconfiguration in k42. In: 6th Linux.Conf.Au (2005)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Arnold, J., Kaashoek, M.F.: Ksplice: automatic rebootless kernel updates. In: Proceedings of the 4th ACM European Conference on Computer Systems, EuroSys 2009, pp. 187\u2013198. ACM, New York (2009)","DOI":"10.1145\/1519065.1519085"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Wahler, M., Oriol, M.: Disruption-free software updates in automation systems. In: Emerging Technology and Factory Automation (ETFA), pp. 1\u20138. IEEE, September 2014","DOI":"10.1109\/ETFA.2014.7005075"},{"key":"3_CR4","unstructured":"Holmbacka, S., Lund, W., Lafond, S., Lilius, J.: Lightweight framework for runtime updating of c-based software in embedded systems. In: Presented as Part of the 5th Workshop on Hot Topics in Software Upgrades. USENIX, Berkeley (2013)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Noubissi, A.C., Iguchi-Cartigny, J., Lanet, J.-L.: Hot updates for Java based smart cards, pp. 168\u2013173, April 2011","DOI":"10.1109\/ICDEW.2011.5767630"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Liu, J., Tong, W.: A framework for dynamic updating of service pack in the Internet of Things. In: 2011 International Conference on Internet of Things (iThings\/CPSCom) and 4th International Conference on Cyber, Physical and Social Computing, pp. 33\u201342 (2011)","DOI":"10.1109\/iThings\/CPSCom.2011.45"},{"key":"3_CR7","unstructured":"Lounas, R., Mezghiche, M., Lanet, J.-L.: An approach for formal verification of updated Java bytecode programs. In: Hedia, B.B., Vladicescu, F.P. (eds.) Proceedings of the 9th Workshop on Verification and Evaluation of Computer and Communication Systems, VECoS, Bucharest, Romania, 10\u201311 September, vol. 1431. CEUR Workshop Proceedings, pp. 51\u201364. CEUR-WS.org (2015)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Charlton, N., Horsfall, B., Reus, B.: Formal reasoning about runtime code update. In: ICDE Workshops, pp. 134\u2013138. IEEE (2011)","DOI":"10.1109\/ICDEW.2011.5767624"},{"key":"3_CR9","series-title":"Representation and Mind Series","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. Representation and Mind Series. The MIT Press, Cambridge (2008)"},{"key":"3_CR10","unstructured":"Common Criteria. https:\/\/www.commoncriteriaportal.org\/ . Accessed 05 June 2016"},{"key":"3_CR11","unstructured":"Secr\u00e9tariat g\u00e9n\u00e9ral de la d\u00e9fense et de la s\u00e9curit\u00e9 nationale. Security requirements for post-delivery code loading. Agence Nationale de la S\u00e9curit\u00e9 des Syst\u00e8mes d\u2019Information, Paris (2015)"},{"key":"3_CR12","unstructured":"Noubissi, A.C.: Mise \u00e1 jour dynamique et scuris\u00e9e de composants syst\u00e9me dans une carte \u00e1 puce. Ph.D. thesis, University of Limoges, France (2011)"},{"key":"3_CR13","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, New York (2003)","edition":"1"},{"issue":"5","key":"3_CR14","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR15","unstructured":"SPIN model checker. http:\/\/spinroot.com\/ . Accessed 05 June 2016"},{"issue":"4","key":"3_CR16","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1109\/TSE.2002.995426","volume":"28","author":"GJ Holzmann","year":"2002","unstructured":"Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE Trans. Softw. Eng. 28(4), 364\u2013377 (2002)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR17","unstructured":"The modex tool user guide. http:\/\/spinroot.com\/modex\/MANUAL.html . Accessed 05 June 2016"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Zhang, M., Ogata, K., Futatsugi, K.: An algebraic approach to formal analysis of dynamic software updating mechanisms. In: Leung, K.R.P.H., Muenchaisri, P. (eds.) 19th Asia-Pacific Software Engineering Conference, APSEC, Hong Kong, China, 4\u20137 December, pp. 664\u2013673. IEEE (2012)","DOI":"10.1109\/APSEC.2012.100"},{"key":"3_CR19","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1016\/j.entcs.2013.02.013","volume":"294","author":"M Zhang","year":"2013","unstructured":"Zhang, M., Ogata, K., Futatsugi, K.: Formalization and verification of behavioral correctness of dynamic software updates. Electr. Notes Theor. Comput. Sci. 294, 12\u201323 (2013)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Neamtiu, I., Hicks, M., Foster, J.S., Pratikakis, P.: Contextual effects for version-consistent dynamic software updating and safe concurrent programming. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 37\u201349. ACM, New York (2008)","DOI":"10.1145\/1328897.1328447"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Anderson, A., Rathke, J.: Migrating protocols in multi-threaded message-passing systems. In: Proceedings of the 2nd International Workshop on Hot Topics in Software Upgrades, HotSWUp 2009, pp. 8:1\u20138:5. ACM, New York (2011)","DOI":"10.1145\/1656437.1656448"},{"key":"3_CR22","unstructured":"Bierman, G., Hicks, M., Sewell, P., Stoyle, G.: Formalizing dynamic software updating. In: On-line Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE), Warsaw, Poland (2003)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Stoyle, G., Hicks, M., Bierman, G., Sewell, P., Neamtiu, I.: Mutatis mutandis: safe and predictable dynamic software updating. ACM Trans. Program. Lang. Syst. 29(4), August 2007","DOI":"10.1145\/1255450.1255455"},{"key":"3_CR24","unstructured":"Murarka, Y.: Online update of concurrent object oriented programs. Ph.D. thesis, Indian Institute of Technology, India (2010)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Murarka, Y., Bellur, U.: Correctness of request executions in online updates of concurrent object oriented programs. In: 15th Asia-Pacific Software Engineering Conference, APSEC 2008, pp. 93\u2013100, December 2008","DOI":"10.1109\/APSEC.2008.33"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-27705-4_22","volume-title":"Verified Software: Theories, Tools, Experiments","author":"CM Hayden","year":"2012","unstructured":"Hayden, C.M., Magill, S., Hicks, M., Foster, N., Foster, J.S.: Specifying and verifying the correctness of dynamic software updates. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 278\u2013293. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-27705-4_22"},{"issue":"3","key":"3_CR27","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1145\/1272998.1273031","volume":"41","author":"K Makris","year":"2007","unstructured":"Makris, K., Ryu, K.D.: Dynamic and adaptive updates of non-quiescent subsystems in commodity operating system kernels. SIGOPS Oper. Syst. Rev. 41(3), 327\u2013340 (2007)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Lv, W., Zuo, X., Wang, L.: Dynamic software updating for onboard software. In: Second International Conference on Intelligent System Design and Engineering Application (ISDEA 2012), pp. 251\u2013253, January 2012","DOI":"10.1109\/ISdea.2012.579"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Zhang, M., Ogata, K., Futatsugi, K.: Towards a formal approach to modeling and verifying the design of dynamic software updates. In: Asia-Pacific Software Engineering Conference (APSEC 2015), pp. 159\u2013166, December 2015","DOI":"10.1109\/APSEC.2015.28"}],"container-title":["Lecture Notes in Computer Science","Risks and Security of Internet and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-54876-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,24]],"date-time":"2022-07-24T20:11:23Z","timestamp":1658693483000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-54876-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319548753","9783319548760"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-54876-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}