{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:14:47Z","timestamp":1740132887498,"version":"3.37.3"},"reference-count":40,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"12","license":[{"start":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T00:00:00Z","timestamp":1701388800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T00:00:00Z","timestamp":1701388800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T00:00:00Z","timestamp":1701388800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100004608","name":"Natural Science Foundation of Jiangsu Province in China","doi-asserted-by":"publisher","award":["BK20191475"],"award-info":[{"award-number":["BK20191475"]}],"id":[{"id":"10.13039\/501100004608","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Intell. Transport. Syst."],"published-print":{"date-parts":[[2023,12]]},"DOI":"10.1109\/tits.2022.3224385","type":"journal-article","created":{"date-parts":[[2022,11,29]],"date-time":"2022-11-29T19:19:26Z","timestamp":1669749566000},"page":"15459-15467","source":"Crossref","is-referenced-by-count":2,"title":["A Formal Approach to Design and Security Verification of Operating Systems for Intelligent Transportation Systems Based on Object Model"],"prefix":"10.1109","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7807-2600","authenticated-orcid":false,"given":"Zhenjiang","family":"Qian","sequence":"first","affiliation":[{"name":"School of Computer Science and Engineering, Changshu Institute of Technology, Suzhou, China"}]},{"given":"Shan","family":"Zhong","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Changshu Institute of Technology, Suzhou, China"}]},{"given":"Gaofei","family":"Sun","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Changshu Institute of Technology, Suzhou, China"}]},{"given":"Xiaoshuang","family":"Xing","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Changshu Institute of Technology, Suzhou, China"}]},{"given":"Yong","family":"Jin","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Changshu Institute of Technology, Suzhou, China"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813637"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813643"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978321"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2020.2992232"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2020.2964410"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2019.2908074"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/800215.806571"},{"article-title":"A verified operating system kernel","year":"1987","author":"Bevier","key":"ref8"},{"volume-title":"Coyotos Website","year":"2021","key":"ref9"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2893177"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522720"},{"volume-title":"Yale Flint Project","year":"2021","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2015.2489184"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2017.2670146"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2016.2569414"},{"key":"ref16","first-page":"1","article-title":"Towards a verified, general-purpose operating system kernel","volume-title":"Proc. 1st NICTA Workshop Operating Syst. Verification","author":"Shapiro"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/319344.319163"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"ref22","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","volume":"2283","author":"Nipkow","year":"2002"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3378426"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421475"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3230627"},{"article-title":"VeriML: A dependently-typed, user-extensible, and language-centric approach to proof assistant","year":"2012","author":"Stampoulis","key":"ref26"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3371088"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3357223.3362739"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3360562"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3485474"},{"key":"ref31","first-page":"2417","article-title":"Blinder: Partition-oblivious hierarchical scheduling","volume-title":"Proc. 30th USENIX Secur.","author":"Yoon"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454097"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_28"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192381"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314595"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3158108"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"}],"container-title":["IEEE Transactions on Intelligent Transportation Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6979\/10339106\/09966324.pdf?arnumber=9966324","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,16]],"date-time":"2024-02-16T19:23:19Z","timestamp":1708111399000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9966324\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12]]},"references-count":40,"journal-issue":{"issue":"12"},"URL":"https:\/\/doi.org\/10.1109\/tits.2022.3224385","relation":{},"ISSN":["1524-9050","1558-0016"],"issn-type":[{"type":"print","value":"1524-9050"},{"type":"electronic","value":"1558-0016"}],"subject":[],"published":{"date-parts":[[2023,12]]}}}