{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,18]],"date-time":"2026-02-18T22:46:08Z","timestamp":1771454768176,"version":"3.50.1"},"reference-count":31,"publisher":"American Institute of Aeronautics and Astronautics (AIAA)","issue":"5","content-domain":{"domain":["arc.aiaa.org"],"crossmark-restriction":true},"short-container-title":["Journal of Aerospace Information Systems"],"published-print":{"date-parts":[[2014,5]]},"DOI":"10.2514\/1.i010096","type":"journal-article","created":{"date-parts":[[2014,9,8]],"date-time":"2014-09-08T17:53:05Z","timestamp":1410198785000},"page":"258-279","update-policy":"https:\/\/doi.org\/10.2514\/aiaa_crossmarkpolicy","source":"Crossref","is-referenced-by-count":31,"title":["Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation"],"prefix":"10.2514","volume":"11","author":[{"given":"Matt","family":"Webster","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, England L69 3BX, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil","family":"Cameron","sequence":"additional","affiliation":[{"name":"Virtual Engineering Centre, Daresbury Laboratory, Warrington, England WA4 4AD, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool L69 3BX, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mike","family":"Jump","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool L69 3BX, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1387","reference":[{"key":"r1","unstructured":"WeibelR. E.HansmanR. J. \u201cSafety Considerations for Operation of Unmanned Aerial Vehicles in the National Airspace System,\u201d Massachusetts Inst. of Technology International Center for Air Transportation TR-ICAT-2005-1, Cambridge, MA, 2005."},{"key":"r2","volume-title":"World Unmanned Aerial Vehicle Systems: 2011 Market Profile and Forecast","author":"Zaloga S. J.","year":"2011"},{"key":"r3","volume-title":"CAP 553: BCAR Section A: Airworthiness Procedures Where the CAA has Primary Responsibility for Type Approval of the Product","year":"2011"},{"key":"r4","volume-title":"CAP 722: Unmanned Aircraft System Operations in UK Airspace\u2014Guidance","year":"2010"},{"key":"r5","unstructured":"WooldridgeM., An Introduction to Multiagent Systems, Wiley, Chester, England, U.K., 2002, p.\u00a023."},{"key":"r6","volume-title":"Unmanned Aircraft Systems (UAS)","year":"2011"},{"key":"r8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24270-0_17"},{"key":"r9","unstructured":"CAP 393 Air Navigation: The Order and the Regulations, Civil Aviation Authority, London, April\u00a02010, http:\/\/www.caa.co.uk\/docs\/33\/CAP393.pdf [retrieved June\u00a02012]."},{"key":"r10","doi-asserted-by":"publisher","DOI":"10.2514\/6.2011-6664"},{"key":"r11","doi-asserted-by":"publisher","DOI":"10.2514\/6.2012-2573"},{"key":"r12","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann G. J.","year":"2004"},{"key":"r14","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-011-0088-x"},{"key":"r15","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(98)00068-X"},{"key":"r18","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2006.17"},{"key":"r21","volume-title":"What is Mathematical Logic?","author":"Crossley J. N.","year":"1972"},{"key":"r22","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2010.88"},{"key":"r23","doi-asserted-by":"publisher","DOI":"10.1145\/2500468.2494558"},{"key":"r25","unstructured":"WebsterM.FisherM.JumpM.CameronN. \u201cModel Checking and the Certification of Autonomous Unmanned Aircraft Systems,\u201d Univ. of Liverpool, Dept. of Computer Science, Rept.\u00a0TR-ULCS-11-001, Liverpool, England, U.K. 2011."},{"key":"r26","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008"},{"key":"r27","volume-title":"Model Checking","author":"Clarke E.","year":"1999"},{"key":"r28","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"r29","doi-asserted-by":"publisher","DOI":"10.1002\/9781119991472"},{"key":"r31","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5804.001.0001","volume-title":"Reasoning about Rational Agents","author":"Wooldridge M.","year":"2000"},{"key":"r35","unstructured":"LiuD. \u201cFormalizing Rules of the Air for Formal Verification of Autonomous UAS,\u201d M.S. Thesis, Univ. of Liverpool, Dept. of Computer Science, Liverpool, England, U.K. 2012."},{"key":"r37","doi-asserted-by":"publisher","DOI":"10.2514\/1.32013"},{"key":"r38","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"r39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_35"},{"key":"r41","doi-asserted-by":"publisher","DOI":"10.2514\/1.49356"},{"key":"r42","first-page":"45","volume-title":"Proceedings of Dependable Robots in Human Environments (DRHE)","author":"Chaudemar J.-C.","year":"2010"},{"key":"r49","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"r51","unstructured":"LapouchnianA. \u201cGoal-Oriented Requirements Engineering: An Overview of the Current Research,\u201d Univ. of Toronto, TR, Toronto, 2005, http:\/\/www.cs.toronto.edu\/~alexei\/pub\/Lapouchnian-Depth.pdf [retrieved 1\u00a0June\u00a02013]."}],"container-title":["Journal of Aerospace Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/arc.aiaa.org\/doi\/pdf\/10.2514\/1.I010096","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T14:45:28Z","timestamp":1746369928000},"score":1,"resource":{"primary":{"URL":"https:\/\/arc.aiaa.org\/doi\/10.2514\/1.I010096"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5]]},"references-count":31,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,5]]}},"alternative-id":["10.2514\/1.I010096"],"URL":"https:\/\/doi.org\/10.2514\/1.i010096","relation":{},"ISSN":["2327-3097"],"issn-type":[{"value":"2327-3097","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5]]},"assertion":[{"value":"2012-11-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-06-18","order":1,"name":"revised","label":"Revised","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-08-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-05-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}