{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:37:18Z","timestamp":1771061838337,"version":"3.50.1"},"reference-count":17,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-9-0179"],"award-info":[{"award-number":["FA8750-12-9-0179"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer"],"published-print":{"date-parts":[[2018,11]]},"DOI":"10.1109\/mc.2018.2876051","type":"journal-article","created":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T19:56:31Z","timestamp":1548446191000},"page":"14-23","source":"Crossref","is-referenced-by-count":29,"title":["A Formal Approach to Constructing Secure Air Vehicle Software"],"prefix":"10.1109","volume":"51","author":[{"given":"Darren","family":"Cofer","sequence":"first","affiliation":[{"name":"Rockwell Collins Advanced Technology Center"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[{"name":"Rockwell Collins Advanced Technology Center"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Backes","sequence":"additional","affiliation":[{"name":"Rockwell Collins Advanced Technology Center"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[{"name":"Computer Science, University of Minnesota"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lee","family":"Pike","sequence":"additional","affiliation":[{"name":"Groq, Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Foltzer","sequence":"additional","affiliation":[{"name":"Fastly"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michal","family":"Podhradsky","sequence":"additional","affiliation":[{"name":"Galois Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"CSIRO, Data61"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ihor","family":"Kuz","sequence":"additional","affiliation":[{"name":"CSIRO, Data61"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[{"name":"CSIRO, Data61"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"University of New South Wales, Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Douglas","family":"Stuart","sequence":"additional","affiliation":[{"name":"Boeing Research and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_3"},{"key":"ref11","year":"2011"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2007.17"},{"key":"ref13","article-title":"Building embedded systems with embedded DSLs (experience report)","author":"hickey","year":"0","journal-title":"Proc Int Conf Functional Programming (ICFP)"},{"key":"ref14","year":"2009","journal-title":"JPL Institutional Coding Standard for the C Programming Language"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"ref16","author":"nipkow","year":"2002","journal-title":"Isabelle\/HOL A Proof Assistant for Higher-Order Logic"},{"key":"ref17","author":"cofer","year":"0","journal-title":"High-assurance cyber military systems (HACMS) 2017"},{"key":"ref4","author":"santamarta","year":"2018","journal-title":"Last Call for SATCOM Security"},{"key":"ref3","article-title":"Feds say that banned researcher commandeered a plane","author":"zetter","year":"2015","journal-title":"Wired"},{"key":"ref6","author":"feiler","year":"2012","journal-title":"Model-Based Engineering with AADL An Introduction to the SAE Architecture Analysis & Design Language"},{"key":"ref5","author":"warwick","year":"2017","journal-title":"DARPA blocks cyberattacks on Unmanned Little Bird in flight"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663177"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2012.173"},{"key":"ref2","author":"teso","year":"0","journal-title":"Aircraft hacking Practical aero series 2013"},{"key":"ref1","article-title":"Comprehensive experimental analyses of automotive attack surfaces","author":"stephen","year":"0","journal-title":"20th USENIX Security Symp"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693137"}],"container-title":["Computer"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/2\/8625905\/08625938.pdf?arnumber=8625938","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T19:45:30Z","timestamp":1651779930000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8625938\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":17,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/mc.2018.2876051","relation":{},"ISSN":["0018-9162","1558-0814"],"issn-type":[{"value":"0018-9162","type":"print"},{"value":"1558-0814","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11]]}}}