{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:04:13Z","timestamp":1750309453100,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T00:00:00Z","timestamp":1730851200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"FFG","award":["881844"],"award-info":[{"award-number":["881844"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,11,6]]},"DOI":"10.1145\/3696355.3699706","type":"proceedings-article","created":{"date-parts":[[2025,1,3]],"date-time":"2025-01-03T11:55:46Z","timestamp":1735905346000},"page":"187-196","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Specifications of Real-Time AUTOSAR-Compliant Operating Systems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-2808-9313","authenticated-orcid":false,"given":"Drona","family":"Nagarajan","sequence":"first","affiliation":[{"name":"EAS, Graz University of Technology, 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":"EAS, 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":"EAS, Graz University of Technology, Graz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,3]]},"reference":[{"key":"e_1_3_3_1_2_2","unstructured":"AUTOSAR. 2022. Software Specification od Operating System. (2022). https:\/\/www.autosar.org\/fileadmin\/standards\/R22-11\/CP\/AUTOSAR_SWS_OS.pdf"},{"key":"e_1_3_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45943-1_13"},{"key":"e_1_3_3_1_4_2","unstructured":"A. Burns. 2013. The Application of the Original Priority Ceiling Protocol to Mixed Criticality Systems."},{"key":"e_1_3_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/CoDIT.2018.8394813"},{"key":"e_1_3_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/550359"},{"key":"e_1_3_3_1_8_2","unstructured":"Elektrobit. [n. d.]. Elektrobit tresos\\(^\\text{®}\\) AutoCoreOS. https:\/\/www.elektrobit.com\/products\/ecu\/eb-tresos\/bsw\/"},{"key":"e_1_3_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.105"},{"key":"e_1_3_3_1_10_2","doi-asserted-by":"crossref","unstructured":"C. Hawblitzel J. Howell M. Kapritsos J.\u00a0R. Lorch B. Parno M.\u00a0L. Roberts S.\u00a0T.\u00a0V. Setty and B. Zill. 2015. IronFleet: proving practical distributed systems correct. Proc. SOSP (2015).","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_3_1_11_2","doi-asserted-by":"crossref","unstructured":"I. Kassios. 2011. The dynamic frames theory. Formal Aspects of Computing (2011).","DOI":"10.1007\/s00165-010-0152-5"},{"key":"e_1_3_3_1_12_2","doi-asserted-by":"crossref","unstructured":"K.\u00a0R.\u00a0M. Leino. 2010. Dafny: an automatic program verifier for functional correctness(LPAR).","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_3_1_13_2","volume-title":"International School on Engineering Trustworthy Software Systems","author":"Leino K.\u00a0Rustan\u00a0M.","year":"2017","unstructured":"K.\u00a0Rustan\u00a0M. Leino. 2017. Modeling Concurrency in Dafny. In International School on Engineering Trustworthy Software Systems."},{"key":"e_1_3_3_1_14_2","unstructured":"Matthew\u00a0John Matias. 2014. Program Verification of FreeRTOS using Microsoft Dafny."},{"key":"e_1_3_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30826-0_2"},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"crossref","unstructured":"L.\u00a0R. Sha R.\u00a0R. Rajkumar and J.\u00a0P. Lehoczky. 1990. Priority Inheritance Protocols: An Approach to Real-Time Synchronization. IEEE Trans. Computers (1990).","DOI":"10.1109\/12.57058"},{"key":"e_1_3_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763028"},{"key":"e_1_3_3_1_18_2","unstructured":"J.\u00a0L. Singleton G.\u00a0T. Leavens H. Rajan and D.\u00a0R. Cok. 2019. Inferring Concise Specifications of APIs. ArXiv (2019)."},{"key":"e_1_3_3_1_19_2","doi-asserted-by":"crossref","unstructured":"H. Witharana Y. Lyu S. Charles and P. Mishra. 2022. A survey on assertion-based hardware verification. ACM Computing Surveys (CSUR) (2022).","DOI":"10.1145\/3510578"},{"key":"e_1_3_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"e_1_3_3_1_21_2","doi-asserted-by":"crossref","unstructured":"L. Zhang and B.\u00a0L. Kaminski. 2022. Quantitative strongest post: a calculus for reasoning about the flow of quantitative information. Proc. ACM Program. Lang.OOPSLA1 (2022).","DOI":"10.1145\/3527331"},{"key":"e_1_3_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.94"}],"event":{"name":"RTNS 2024: The 32nd International Conference on Real-Time Networks and Systems","acronym":"RTNS 2024","location":"Porto Portugal"},"container-title":["Proceedings of the 32nd International Conference on Real-Time Networks and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696355.3699706","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696355.3699706","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:10:11Z","timestamp":1750295411000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696355.3699706"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,6]]},"references-count":21,"alternative-id":["10.1145\/3696355.3699706","10.1145\/3696355"],"URL":"https:\/\/doi.org\/10.1145\/3696355.3699706","relation":{},"subject":[],"published":{"date-parts":[[2024,11,6]]},"assertion":[{"value":"2025-01-03","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}