{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:25:33Z","timestamp":1742984733452,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":20,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819606160"},{"type":"electronic","value":"9789819606177"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-981-96-0617-7_12","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T14:47:28Z","timestamp":1732805248000},"page":"199-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Analysis of\u00a0FreeRTOS Scheduler on\u00a0ARM Cortex-M4 Cores"],"prefix":"10.1007","author":[{"given":"Chen-Kai","family":"Lin","sequence":"first","affiliation":[]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-43144-4_4","volume-title":"Interactive Theorem Proving","author":"J Andronick","year":"2016","unstructured":"Andronick, J., Lewis, C., Matichuk, D., Morgan, C., Rizkallah, C.: Proof of OS scheduling behavior in the presence of interrupt-induced concurrency. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 52\u201368. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_4"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Asadollah, S.A., Sundmark, D., Eldh, S., Hansson, H.: A runtime verification tool for detecting concurrency bugs in freertos embedded software. In: 2018 17th International Symposium on Parallel and Distributed Computing (ISPDC), pp. 172\u2013179 (2018). https:\/\/doi.org\/10.1109\/ISPDC2018.2018.00032","DOI":"10.1109\/ISPDC2018.2018.00032"},{"key":"12_CR3","unstructured":"AspenCore: 2019 embedded markets study. Technical report, EE Times and Embedded, March 2019. https:\/\/www.embedded.com\/wp-content\/uploads\/2019\/11\/EETimes_Embedded_2019_Embedded_Markets_Study.pdf"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Chandrasekaran, P., Shibu\u00a0Kumar, K.B., Minz, R.L., D\u2019Souza, D., Meshram, L.: A multi-core version of freertos verified for datarace and deadlock freedom. In: 2014 Twelfth ACM\/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 62\u201371 (2014). https:\/\/doi.org\/10.1109\/MEMCOD.2014.6961844","DOI":"10.1109\/MEMCOD.2014.6961844"},{"issue":"1","key":"12_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s00165-014-0308-9","volume":"27","author":"S Cheng","year":"2014","unstructured":"Cheng, S., Woodcock, J., D\u2019Souza, D.: Using formal reasoning on a model of tasks for FreeRTOS. Formal Aspects Comput. 27(1), 167\u2013192 (2014). https:\/\/doi.org\/10.1007\/s00165-014-0308-9","journal-title":"Formal Aspects Comput."},{"key":"12_CR6","unstructured":"Chong, N.: Ensuring the memory safety of freertos part 1, Feburary 2020. https:\/\/www.freertos.org\/2020\/02\/ensuring-the-memory-safety-of-freertos-part-1.html"},{"key":"12_CR7","unstructured":"Chong, N., Jacobs, B.: Formally verifying freertos\u2019 interprocess communication mechanism. In: Proceedings of the Embedded World Conference. N\u00fcrnberg, Germany, March 2021, https:\/\/www.amazon.science\/publications\/formally-verifying-freertos-interprocess-communication-mechanism"},{"key":"12_CR8","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"de Oliveira, D.B., de Oliveira, R.S., Cucinotta, T.: Untangling the intricacies of thread synchronization in the preempt_rt linux kernel. In: 2019 IEEE 22nd International Symposium on Real-Time Distributed Computing (ISORC), pp.\u00a01\u20139. IEEE, Valencia, Spain (2019)","DOI":"10.1109\/ISORC.2019.00012"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-25423-4_11","volume-title":"Formal Methods and Software Engineering","author":"S Divakaran","year":"2015","unstructured":"Divakaran, S., D\u2019Souza, D., Kushwah, A., Sampath, P., Sridhar, N., Woodcock, J.: Refinement-based verification of the FreeRTOS scheduler in VCC. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 170\u2013186. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_11"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 170\u2013182. Association for Computing Machinery, New York (2008). https:\/\/doi.org\/10.1145\/1375581.1375603","DOI":"10.1145\/1375581.1375603"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Ferreira, J.F., He, G., Qin, S.: Automated verification of the freertos scheduler in hip\/sleek. In: 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering, pp. 51\u201358 (2012). https:\/\/doi.org\/10.1109\/TASE.2012.45","DOI":"10.1109\/TASE.2012.45"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-030-25543-5_28","volume-title":"Computer Aided Verification","author":"X Guo","year":"2019","unstructured":"Guo, X., Lesourd, M., Liu, M., Rieg, L., Shao, Z.: Integrating formal schedulability analysis into a verified OS kernel. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 496\u2013514. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_28"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Guo, X., Lin, H.H., Aoki, T., Chiba, Y.: A reusable framework for modeling and verifying in-vehicle networking systems in the presence of can and flexray. In: 2017 24th Asia-Pacific Software Engineering Conference (APSEC), pp. 140\u2013149 (2017). https:\/\/doi.org\/10.1109\/APSEC.2017.20","DOI":"10.1109\/APSEC.2017.20"},{"key":"12_CR15","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2021.111033","volume":"181","author":"PE Hladik","year":"2021","unstructured":"Hladik, P.E., Ingrand, F., Dal Zilio, S., Tekin, R.: Hippo: a formal-model execution engine to control and verify critical real-time systems. J. Syst. Softw. 181, 111033 (2021). https:\/\/doi.org\/10.1016\/j.jss.2021.111033","journal-title":"J. Syst. Softw."},{"issue":"5","key":"12_CR16","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-030-30446-1_17","volume-title":"Software Engineering and Formal Methods","author":"DB de Oliveira","year":"2019","unstructured":"de Oliveira, D.B., Cucinotta, T., de Oliveira, R.S.: Efficient formal verification for the linux kernel. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 315\u2013332. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_17"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Sanan, D., Yang, L., Yongwang, Z., Zhenchang, X., Hinchey, M.: Verifying freertos\u2019 cyclic doubly linked list implementation: from abstract specification to machine code. In: 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 120\u2013129. IEEE Computer Society, Los Alamitos, December 2015. https:\/\/doi.org\/10.1109\/ICECCS.2015.23","DOI":"10.1109\/ICECCS.2015.23"},{"key":"12_CR19","unstructured":"Tsafrir, D., Etsion, Y., Feitelson, D.G.: Secretly monopolizing the CPU without superuser privileges. In: 16th USENIX Security Symposium (USENIX Security 07). USENIX Association, Boston, MA, August 2007"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-41540-6_4","volume-title":"Computer Aided Verification","author":"F Xu","year":"2016","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 59\u201379. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_4"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-0617-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T15:09:36Z","timestamp":1732806576000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-0617-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9789819606160","9789819606177"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-0617-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hiroshima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.icfem2024.info\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}