{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:06:49Z","timestamp":1750309609188,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"The Austrian Research Promotion Agency (FFG)","award":["881844"],"award-info":[{"award-number":["881844"]}]},{"name":"TU Graz Open Access Publishing Fund"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,31]]},"DOI":"10.1145\/3672608.3707867","type":"proceedings-article","created":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:26:21Z","timestamp":1747247181000},"page":"2007-2016","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modeling and Verification of Low-Level AUTOSAR OS Specifications: Towards Portability and Correctness"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5580-348X","authenticated-orcid":false,"given":"Vignesh","family":"Manjunath","sequence":"first","affiliation":[{"name":"Graz University of Technology, Graz, Austria"},{"name":"Pro2Future GmbH, Graz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0691-6119","authenticated-orcid":false,"given":"Tobias","family":"Scheipel","sequence":"additional","affiliation":[{"name":"Graz University of Technology, Graz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3716-2682","authenticated-orcid":false,"given":"Marcel","family":"Baunach","sequence":"additional","affiliation":[{"name":"Graz University of Technology, Graz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,5,14]]},"reference":[{"volume-title":"Modeling in Event-B: system and software engineering","author":"Abrial Jean-Raymond","key":"e_1_3_2_1_1_1","unstructured":"Jean-Raymond Abrial. 2010. Modeling in Event-B: system and software engineering. Cambridge University Press."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-024-00743-4"},{"key":"e_1_3_2_1_4_1","unstructured":"Infineon Technologies AG. 2021. AURIX\u2122 TC3xx User Manual Part-1."},{"key":"e_1_3_2_1_5_1","unstructured":"Infineon Technologies AG. 2021. AURIX\u2122 TC3xx User Manual Part-2."},{"key":"e_1_3_2_1_6_1","unstructured":"Infineon Technologies AG. 2023. 32-bit AURIX\u2122 TriCore\u2122 Microcontroller. https:\/\/www.infineon.com\/cms\/en\/product\/microcontroller\/32-bit-tricore-microcontroller\/"},{"key":"e_1_3_2_1_7_1","unstructured":"AUTOSAR. 2022. Specification of Operating System. https:\/\/www.autosar.org\/fileadmin\/standards\/R22-11\/CP\/AUTOSAR_SWS_OS.pdf"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04468-7_16"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2006.355432"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/CoDIT.2018.8394813"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1201\/9781351255790"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-40436-8_13"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2018.00017"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2021.3058394"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30446-1_17"},{"key":"e_1_3_2_1_16_1","volume-title":"1st Int. Workshop About Sets and Tools (SETS","author":"D\u00e9harbe David","year":"2014","unstructured":"David D\u00e9harbe, Pascal Fontaine, Yoann Guyot, and Laurent Voisin. 2014. Introduction to the Integration of SMT-Solvers in Rodin. In 1st Int. Workshop About Sets and Tools (SETS 2014). ABZ."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2018.00028"},{"key":"e_1_3_2_1_18_1","unstructured":"Event-B. 2023. Event-B Summary. https:\/\/wiki.event-b.org\/images\/EventBSummary.pdf"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.105"},{"key":"e_1_3_2_1_20_1","unstructured":"Elektrobit Automotive GmbH. 2022. AutoCore OS Classic AUTOSAR Operating System. https:\/\/www.elektrobit.com\/products\/ecu\/eb-tresos\/operating-systems\/"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58768-0_9"},{"key":"e_1_3_2_1_22_1","volume-title":"OSDI","volume":"16","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: an extensible architecture for building certified concurrent OS kernels. In OSDI, Vol. 16."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3073398"},{"key":"e_1_3_2_1_25_1","unstructured":"RISC-V International. 2023. https:\/\/riscv.org\/"},{"volume-title":"The RISC-V Instruction Set - Manual","author":"International RISC-V","key":"e_1_3_2_1_26_1","unstructured":"RISC-V International. 2024. The RISC-V Instruction Set - Manual Volume I."},{"key":"e_1_3_2_1_27_1","volume-title":"Proc. of the Systems Eng. Infrastructure Conf.","author":"Jastram Michael","year":"2010","unstructured":"Michael Jastram. 2010. ProR, an open source platform for requirements engineering based on RIF. In Proc. of the Systems Eng. Infrastructure Conf. (2010)."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"volume-title":"The Real Time Kernel","author":"Labrosse Jean","key":"e_1_3_2_1_29_1","unstructured":"Jean Labrosse. 2002. MicroC\/OS-II: The Real Time Kernel. CRC Press."},{"key":"e_1_3_2_1_30_1","volume-title":"Formal Methods Applied to Complex Systems: Implementation of the B Method","author":"Lecomte Thierry","year":"2014","unstructured":"Thierry Lecomte. 2014. Atelier B. Formal Methods Applied to Complex Systems: Implementation of the B Method (2014)."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2024.103220"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-023-01144-y"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-98464-9_8"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-10-4154-9_56"},{"key":"e_1_3_2_1_36_1","unstructured":"Event-B Notation. 2007. Event-B notation. https:\/\/web-archive.southampton.ac.uk\/deploy-eprints.ecs.soton.ac.uk\/11\/3\/notation-1.5.pdf"},{"key":"e_1_3_2_1_37_1","unstructured":"OSEK\/VDX. 2005. Operating System Specification 2.2.3. https:\/\/www.irisa.fr\/alf\/downloads\/puaut\/TPNXT\/images\/os223.pdf"},{"key":"e_1_3_2_1_38_1","unstructured":"PikeOS. 2024. PikeOS Certifiable RTOS & Hypervisor. Retrieved Jan. 1 2024 from https:\/\/www.sysgo.com\/pikeos"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"e_1_3_2_1_40_1","volume-title":"Tim Sagaster, and Marcel Baunach.","author":"Scheipel Tobias","year":"2022","unstructured":"Tobias Scheipel, Leandro Batista Ribeiro, Tim Sagaster, and Marcel Baunach. 2022. Smartos: An OS architecture for sustainable embedded systems. GI Fachgruppentreffen Betriebssysteme (2022)."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS20050.2012.6299224"},{"key":"e_1_3_2_1_42_1","volume-title":"Proc. of the 5th Rodin User & Developer Workshop","author":"Snook Colin","year":"2014","unstructured":"Colin Snook. 2014. iUML-B Statemachines. Proc. of the 5th Rodin User & Developer Workshop (2014)."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1125808.1125811"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-021-00312-y"}],"event":{"name":"SAC '25: 40th ACM\/SIGAPP Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Catania International Airport Catania Italy","acronym":"SAC '25"},"container-title":["Proceedings of the 40th ACM\/SIGAPP Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672608.3707867","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3672608.3707867","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:33Z","timestamp":1750298253000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3672608.3707867"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":43,"alternative-id":["10.1145\/3672608.3707867","10.1145\/3672608"],"URL":"https:\/\/doi.org\/10.1145\/3672608.3707867","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]},"assertion":[{"value":"2025-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}