{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:01:31Z","timestamp":1740132091878,"version":"3.37.3"},"reference-count":53,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"China HGJ Project","award":["2017ZX01038102-002"],"award-info":[{"award-number":["2017ZX01038102-002"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61532019","61502171"],"award-info":[{"award-number":["61532019","61502171"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Rel."],"published-print":{"date-parts":[[2019,9]]},"DOI":"10.1109\/tr.2018.2863744","type":"journal-article","created":{"date-parts":[[2018,9,12]],"date-time":"2018-09-12T18:48:18Z","timestamp":1536778098000},"page":"1117-1133","source":"Crossref","is-referenced-by-count":5,"title":["Toward a Unified Executable Formal Automobile OS Kernel and Its Applications"],"prefix":"10.1109","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5181-5037","authenticated-orcid":false,"given":"Xiaoran","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-2902","authenticated-orcid":false,"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","first-page":"3r","article-title":"AUTOSAR Methodology","volume":"2","year":"2009","journal-title":"AUTOSAR Standard v1"},{"key":"ref38","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/S1571-0661(05)80134-3","article-title":"Real-time Maude: A tool for simulating and analyzing real-time and hybrid systems","volume":"36","author":"\u00f6lveczky","year":"2000","journal-title":"Electr Notes Theor Comput Sci"},{"journal-title":"Programming in the Osek\/Vdx Environment","year":"2001","author":"lemieux","key":"ref33"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2014.52"},{"year":"0","key":"ref31","article-title":"IELE: A new virtual machine for the blockchain"},{"article-title":"Ethereum: A secure decentralised generalised transaction ledger","year":"2014","author":"wood","key":"ref30"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.12"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2015.7102612"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2011.11"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32943-2_15"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.21236\/ADA418413"},{"year":"2005","key":"ref1","article-title":"OSEK\/VDX operating system specification"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1049\/ic:19981079"},{"key":"ref22","first-page":"73","article-title":"Logical semantics for CafeOBJ","volume":"93","author":"diaconescu","year":"1992","journal-title":"Science"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.10.003"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82552-6"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"ref51","first-page":"481","article-title":"Csimpl: A rely-guarantee-based framework for verifying concurrent programs","author":"san\u00e1n","year":"0","journal-title":"Proc Int Conf Tools and Algorithms Constr and Anal Syst"},{"key":"ref53","first-page":"74","article-title":"Semantics-based program verifiers for all languages","author":"?tef?nescu","year":"0","journal-title":"Proc 31st Conf Object-Oriented Program Syst Lang Appl"},{"key":"ref52","first-page":"653","article-title":"Certikos: An extensible architecture for building certified concurrent OS kernels","author":"gu","year":"0","journal-title":"Proc USENIX Symp on Operating System Design and Implementation"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_4"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16164-3_5"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12904-4_16"},{"key":"ref16","first-page":"212","article-title":"Dynamic priority inversion avoidance in real-time operating systems","author":"huang","year":"0","journal-title":"Proc Int Conf Parallel Distrib Process Techn Appl"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2011.26"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0449-6"},{"year":"2009","key":"ref19","article-title":"OSEK\/VDX operating system specification"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.105"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2013.49"},{"key":"ref6","first-page":"295","article-title":"Evaluation of Maude as a test generation engine for automotive operating systems","volume":"1","author":"choi","year":"0","journal-title":"Proc Asia-Pacific Software Eng Conf"},{"key":"ref5","first-page":"305","article-title":"Constraint specification and test generation for OSEK\/VDX-based operating systems","author":"choi","year":"0","journal-title":"Proc 11th Int Conf Formal Eng Methods"},{"journal-title":"Road Vehicles - Functional safety - Part 1 to Part 10","year":"2011","key":"ref8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40561-7_21"},{"key":"ref49","first-page":"165","article-title":"Ironclad apps: End-to-end security via automated full-system verification","author":"hawblitzel","year":"0","journal-title":"Proc USENIX Symp on Operating System Design and Implementation"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/SIES.2007.4297340"},{"key":"ref46","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1002\/stvr.422","article-title":"Verification support for ARINC-653-based avionics software","volume":"21","author":"de la c\u00e1mara","year":"2011","journal-title":"Softw Test Verif Rel"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2016.2569414"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"ref47","article-title":"Formalization and verification of AUTOSAR OS standards memory protection","author":"trinh","year":"0","journal-title":"Proc 7th Int Symp Theoretical Aspects Softw Eng"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"ref41","article-title":"Formal specification and verification of separation kernels: An overview","author":"zhao","year":"2015","journal-title":"arXiv 1508 07066"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2017.2672983"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_26"}],"container-title":["IEEE Transactions on Reliability"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/24\/8821425\/08462763.pdf?arnumber=8462763","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,1]],"date-time":"2022-09-01T05:31:33Z","timestamp":1662010293000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8462763\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9]]},"references-count":53,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tr.2018.2863744","relation":{},"ISSN":["0018-9529","1558-1721"],"issn-type":[{"type":"print","value":"0018-9529"},{"type":"electronic","value":"1558-1721"}],"subject":[],"published":{"date-parts":[[2019,9]]}}}