{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:44:30Z","timestamp":1747248270175,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030587673"},{"type":"electronic","value":"9783030587680"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-58768-0_9","type":"book-chapter","created":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:02:48Z","timestamp":1599825768000},"page":"155-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Formal Modeling Approach for Portable Low-Level OS Functionality"],"prefix":"10.1007","author":[{"given":"Renata Martins","family":"Gomes","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3484-5584","authenticated-orcid":false,"given":"Bernhard","family":"Aichernig","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3716-2682","authenticated-orcid":false,"given":"Marcel","family":"Baunach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,8]]},"reference":[{"key":"9_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, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Alkhammash, E.H., Butler, M.J., Cristea, C.: Modeling guidelines of FreeRTOS in Event-B. In: International Conference on Communication, Management and Information Technology, pp. 453\u2013462. CRC Press (2017)","DOI":"10.1201\/9781315155241-15"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Baumann, C., Schwarz, O., Dam, M.: Compositional verification of security properties for embedded execution platforms. In: K\u00fchne, U., Danger, J.L., Guilley, S. (eds.) 6th International Workshop on Security Proofs for Embedded Systems, PROOFS 2017. EPiC Series in Computing, vol. 49, pp. 1\u201316. EasyChair (2017). https:\/\/doi.org\/10.29007\/h4rv . https:\/\/easychair.org\/publications\/paper\/wkpS","DOI":"10.29007\/h4rv"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Boano, C.A., R\u00f6mer, K., Bloem, R., Witrisal, K., Baunach, M., Horn, M.: Dependability for the Internet of Things\u2013from dependable networking in harsh environments to a holistic view on dependability. e & i Elektrotechnik und Informationstechnik 133(7), 304\u2013309 (2016). https:\/\/doi.org\/10.1007\/s00502-016-0436-4","DOI":"10.1007\/s00502-016-0436-4"},{"key":"9_CR5","unstructured":"Borghorst, H., Bieling, K., Spinkczyk, O.: Towards versatile models for contemporary hardware platforms. In: 12th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications, OSPERT 2016, pp. 7\u20139, July 2016"},{"key":"9_CR6","unstructured":"Brandenburg, B.B.: The case of an opinionated, theory-oriented real-time operating system. In: NGOSCPS 2019, April 2019"},{"issue":"1","key":"9_CR7","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":"9_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-967-5","volume-title":"Formal Refinement for Operating System Kernels","author":"ID Craig","year":"2007","unstructured":"Craig, I.D.: Formal Refinement for Operating System Kernels. Springer, London (2007). https:\/\/doi.org\/10.1007\/978-1-84628-967-5"},{"key":"9_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-718-3","volume-title":"Formal Models of Operating System Kernels","author":"ID Craig","year":"2010","unstructured":"Craig, I.D.: Formal Models of Operating System Kernels, 1st edn. Springer, London (2010). https:\/\/doi.org\/10.1007\/978-1-84628-718-3","edition":"1"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-319-91271-4_16","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"M Dalvandi","year":"2018","unstructured":"Dalvandi, M., Butler, M., Rezazadeh, A., Salehi Fathabadi, A.: Verifiable code generation from scheduled Event-B models. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 234\u2013248. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91271-4_16"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Danmin, C., Yue, S., Zhiguo, C.: A formal specification in B of an operating system. Open Cybern. Syst. J. 9(1) (2015)","DOI":"10.2174\/1874110X01509011125"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Dhote, S., Charjan, P., Phansekar, A., Hegde, A., Joshi, S., Joshi, J.: Using FPGA-SoC interface for low cost IoT based image processing. In: 2016 International Conference on Advances in Computing, Communications and Informatics (ICACCI), pp. 1963\u20131968, September 2016. https:\/\/doi.org\/10.1109\/ICACCI.2016.7732339","DOI":"10.1109\/ICACCI.2016.7732339"},{"key":"9_CR13","unstructured":"Event-B: Event-B and the Rodin Platform. www.event-b.org"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Fathabadi, A.S., et al.: A model-based framework for software portability and verification in embedded power management systems. J. Syst. Archit. 82, 12\u201323 (2018). https:\/\/doi.org\/10.1016\/j.sysarc.2017.12.001 . http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1383762117305234","DOI":"10.1016\/j.sysarc.2017.12.001"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Fr\u00fchwirth, T., Krammer, L., Kastner, W.: Dependability demands and state of the art in the internet of things. In: 2015 IEEE 20th Conference on Emerging Technologies Factory Automation (ETFA), pp. 1\u20134, September 2015. https:\/\/doi.org\/10.1109\/ETFA.2015.7301592","DOI":"10.1109\/ETFA.2015.7301592"},{"key":"9_CR16","unstructured":"General Dynamics C4 Systems: The seL4 microkernel (2016). https:\/\/sel4.systems\/ . Accessed 05 Feb 2020"},{"key":"9_CR17","unstructured":"Gomes, R.M., Baunach, M., Malenko, M., Ribeiro, L.B., Mauroner, F.: A co-designed RTOS and MCU concept for dynamically composed embedded systems. In: OSPERT 2017 (2017)"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Gomes, T., Pinto, S., Gomes, T., Tavares, A., Cabral, J.: Towards an FPGA-based edge device for the Internet of Things. In: 2015 IEEE 20th Conference on Emerging Technologies Factory Automation (ETFA), pp. 1\u20134, September 2015. https:\/\/doi.org\/10.1109\/ETFA.2015.7301601","DOI":"10.1109\/ETFA.2015.7301601"},{"key":"9_CR19","unstructured":"Goranko, V., Galton, A.: Temporal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2015 edn. (2015). https:\/\/plato.stanford.edu\/archives\/win2015\/entries\/logic-temporal\/"},{"issue":"5","key":"9_CR20","doi-asserted-by":"publisher","first-page":"720","DOI":"10.1109\/JIOT.2015.2505901","volume":"3","author":"O Hahm","year":"2016","unstructured":"Hahm, O., Baccelli, E., Petersen, H., Tsiftes, N.: Operating systems for low-end devices in the Internet of Things: a survey. IEEE Internet Things J. 3(5), 720\u2013734 (2016). https:\/\/doi.org\/10.1109\/JIOT.2015.2505901","journal-title":"IEEE Internet Things J."},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Hu, J., Lu, E., Holland, D.A., Kawaguchi, M., Chong, S., Seltzer, M.I.: Trials and tribulations in synthesizing operating systems. In: Proceedings of the 10th Workshop on Programming Languages and Operating Systems, PLOS 2019, pp. 67\u201373. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3365137.3365401","DOI":"10.1145\/3365137.3365401"},{"key":"9_CR22","unstructured":"Texas Instruments: MSP430 ultra-low-power sensing and measurement MCUs (2019). http:\/\/www.ti.com\/microcontrollers\/msp430-ultra-low-power-mcus\/overview\/overview.html"},{"key":"9_CR23","unstructured":"Jastram, M., Butler, P.M.: Rodin User\u2019s Handbook: Covers Rodin vol. 2.8, USA (2014)"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1) (2014). https:\/\/doi.org\/10.1145\/2560537","DOI":"10.1145\/2560537"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3(2), 125\u2013143 (1977). https:\/\/doi.org\/10.1109\/TSE.1977.229904","DOI":"10.1109\/TSE.1977.229904"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008). https:\/\/doi.org\/10.1007\/s10009-007-0063-9","DOI":"10.1007\/s10009-007-0063-9"},{"key":"9_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z Manna","year":"2012","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-030-03418-4_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Modeling","author":"D M\u00e9ry","year":"2018","unstructured":"M\u00e9ry, D.: Modelling by patterns for correct-by-construction process. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11244, pp. 399\u2013423. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03418-4_24"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-030-03427-6_19","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"E Novikov","year":"2018","unstructured":"Novikov, E., Zakharov, I.: Verification of operating system monolithic kernels without extensions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 230\u2013248. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_19"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46\u201357, October 1977. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Popp, M., Moreira, O., Yedema, W., Lindwer, M.: Automatic HAL generation for embedded multiprocessor systems. In: Proceedings of the 13th International Conference on Embedded Software, EMSOFT 2016, ACM, New York (2016). https:\/\/doi.org\/10.1145\/2968478.2968493","DOI":"10.1145\/2968478.2968493"},{"key":"9_CR32","unstructured":"RISC-V Foundation: RISC-V. https:\/\/riscv.org\/"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/11955757_14","volume-title":"B 2007: Formal Specification and Development in B","author":"B Stoddart","year":"2006","unstructured":"Stoddart, B., Cansell, D., Zeyda, F.: Modelling and proof analysis of interrupt driven scheduling. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 155\u2013170. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11955757_14"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Su, W., Abrial, J.R., Pu, G., Fang, B.: Formal development of a real-time operating system memory manager. In: 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS). IEEE, December 2015. https:\/\/doi.org\/10.1109\/iceccs.2015.24","DOI":"10.1109\/iceccs.2015.24"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Syeda, H.T., Klein, G.: Formal reasoning under cached address translation. J. Autom. Reason. 64, 911\u2013945 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09539-7","DOI":"10.1007\/s10817-019-09539-7"},{"issue":"1","key":"9_CR36","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1109\/MS.2017.26","volume":"34","author":"A Taivalsaari","year":"2017","unstructured":"Taivalsaari, A., Mikkonen, T.: A roadmap to the programmable world: software challenges in the IoT era. IEEE Softw. 34(1), 72\u201380 (2017). https:\/\/doi.org\/10.1109\/MS.2017.26","journal-title":"IEEE Softw."},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Verhulst, E., Boute, R.T., Faria, J.M.S., Sputh, B., Mezhuyev, V.: Formal Development of a Network-Centric RTOS. Springer, Boston (2011). https:\/\/doi.org\/10.1007\/978-1-4419-9736-4","DOI":"10.1007\/978-1-4419-9736-4"},{"key":"9_CR38","unstructured":"Waterman, A., Asanovi\u0107, K.: The RISC-V instruction set manual volume I: user-level ISA version 2.2, May 2017. https:\/\/riscv.org\/specifications"},{"key":"9_CR39","unstructured":"Waterman, A., Lee, Y., Avizienis, R., Patterson, D.A., Asanovi\u0107, K.: The RISC-V instruction set manual volume II: privileged architecture version 1.7. Technical report UCB\/EECS-2015-49, EECS Department, University of California, Berkeley, May 2015. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2015\/EECS-2015-49.html"},{"key":"9_CR40","unstructured":"Wright, S.: Formal construction of instruction set architectures. Ph.D. thesis, University of Bristol (2009). http:\/\/www.cs.bris.ac.uk\/Publications\/Papers\/2001121.pdf"},{"key":"9_CR41","unstructured":"Wright, S.: Automatic generation of C from Event-B. In: Workshop on Integration of Model-Based Formal Methods and Tools, p. 14 (2009)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58768-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,31]],"date-time":"2021-03-31T23:24:44Z","timestamp":1617233084000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-58768-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030587673","9783030587680"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58768-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/event.cwi.nl\/sefm2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}