{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:12:16Z","timestamp":1762459936096},"reference-count":22,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.329.3","type":"journal-article","created":{"date-parts":[[2020,12,2]],"date-time":"2020-12-02T13:09:52Z","timestamp":1606914592000},"page":"23-30","source":"Crossref","is-referenced-by-count":9,"title":["From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project"],"prefix":"10.4204","volume":"329","author":[{"given":"Aaron","family":"Dutle","sequence":"first","affiliation":[{"name":"NASA"}]},{"given":"C\u00e9sar","family":"Mu\u00f1oz","sequence":"additional","affiliation":[{"name":"NASA"}]},{"given":"Esther","family":"Conrad","sequence":"additional","affiliation":[{"name":"NASA"}]},{"given":"Alwyn","family":"Goodloe","sequence":"additional","affiliation":[{"name":"NASA"}]},{"given":"Laura","family":"Titolo","sequence":"additional","affiliation":[{"name":"National Institute of Aerospace"}]},{"given":"Ivan","family":"Perez","sequence":"additional","affiliation":[{"name":"National Institute of Aerospace"}]},{"given":"Swee","family":"Balachandran","sequence":"additional","affiliation":[{"name":"National Institute of Aerospace"}]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[{"name":"NASA"}]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[{"name":"KBR Inc."}]},{"given":"Thomas","family":"Pressburger","sequence":"additional","affiliation":[{"name":"NASA"}]}],"member":"2720","published-online":{"date-parts":[[2020,12,3]]},"reference":[{"key":"BMCFPDASC2018","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/DASC.2018.8569752","article-title":"Independent Configurable Architecture for Reliable Operation of Unmanned Systems with Distributed On-Board Services","volume-title":"Proceedings of the 37th Digital Avionics Systems Conference (DASC 2018)","author":"Balachandran","year":"2018"},{"key":"introRV","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","article-title":"Introduction to Runtime Verification","volume-title":"Lectures on Runtime Verification - Introductory and Advanced Topics","volume":"10457","author":"Bartocci","year":"2018"},{"key":"CauwelsHHJR20","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-030-59155-7_26","article-title":"Integrating Runtime Verification into an Automated UAS Traffic Management System","volume-title":"International workshop on moDeling, vErification and Testing of dEpendable CriTical systems, DETECT 2020","author":"Cauwels","year":"2020"},{"key":"2012:cofer:agree","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","article-title":"Compositional Verification of Architectural Models","volume-title":"Proceedings of the 4th International NASA Formal Methods Symposium (NFM 2012)","volume":"7226","author":"Cofer","year":"2012"},{"key":"CMHNB2016DASC","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/DASC.2016.7778033","article-title":"ICAROUS: Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems","volume-title":"Proceedings of the 35th Digital Avionics Systems Conference (DASC 2016)","author":"Consiglio","year":"2016"},{"key":"cook2018","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-96145-3_3","article-title":"Formal Reasoning About the Security of Amazon Web Services","volume-title":"Computer Aided Verification","author":"Cook","year":"2018"},{"key":"2017:fifarek:spear2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-319-57288-8_30","article-title":"SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements","volume-title":"Proceedings of the 9th International NASA Formal Methods Symposium (NFM 2017)","volume":"10227","author":"Fifarek","year":"2017"},{"key":"GiannakopoulouP20a","article-title":"Formal Requirements Elicitation with FRET","volume-title":"Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020)","author":"Giannakopoulou","year":"2020"},{"key":"GiannakopoulouP20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-030-44429-7_2","article-title":"Generation of Formal Requirements from Structured Natural Language","volume-title":"26th International Working Conference on Requirements Engineering: Foundation for Software Quality, REFSQ 2020","volume":"12045","author":"Giannakopoulou","year":"2020"},{"key":"2008:havelund:verifyyourruns","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-540-69149-5_40","volume-title":"Verify Your Runs","volume":"4171","author":"Havelund","year":"2008"},{"key":"Julian2019","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/DASC43569.2019.9081748","article-title":"Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems","author":"Julian","year":"2019","journal-title":"2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC)"},{"key":"kaivola2009","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-02658-4_32","article-title":"Replacing Testing with Formal Verification in Intel^89.5CoreTM i7 Processor Execution Engine Validation","volume-title":"Computer Aided Verification","author":"Kaivola","year":"2009"},{"key":"Katz2019","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","article-title":"The Marabou Framework for Verification and Analysis of Deep Neural Networks","volume-title":"Computer Aided Verification","author":"Katz","year":"2019"},{"issue":"4","key":"Koymans90","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying Real-time Properties with Metric Temporal Logic","volume":"2","author":"Koymans","year":"1990","journal-title":"Real-Time Syst."},{"key":"LaroussinieMS02","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1109\/LICS.2002.1029846","article-title":"Temporal Logic with Forgettable Past","volume-title":"LICS\u201902: Proceeding of Logic in Computer Science 2002","author":"Laroussinie","year":"2002"},{"key":"pvs","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","article-title":"PVS: A Prototype Verification System","volume-title":"Proceeding of the 11th International Conference on Automated Deduction (CADE)","volume":"607","author":"Owre","year":"1992"},{"key":"2010:pike:copilot","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-16612-9_26","article-title":"Copilot: A Hard Real-Time Runtime Monitor","volume-title":"Proceedings of the First International Conference on Runtime Verification (RV 2010)","volume":"6418","author":"Pike","year":"2010"},{"issue":"4","key":"2013:pike","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s11334-013-0223-x","article-title":"Copilot: monitoring embedded systems","volume":"9","author":"Pike","year":"2013","journal-title":"Innovations in Systems and Software Engineering"},{"key":"1977:pnueli","series-title":"SFCS '77","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/SFCS.1977.32","article-title":"The Temporal Logic of Programs","volume-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science","author":"Pnueli","year":"1977"},{"key":"ReinbacherRS14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-54862-8_24","article-title":"Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems","volume-title":"Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014)","volume":"8413","author":"Reinbacher","year":"2014"},{"key":"SchumannMR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-319-23820-3_15","article-title":"R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems","volume-title":"Proceedings of the 6th International Conference on Runtime Verification (RV 2015)","volume":"9333","author":"Schumann","year":"2015"},{"key":"Souyris2009","series-title":"FM '09","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_34","article-title":"Formal Verification of Avionics Software Products","volume-title":"Proceedings of the 2nd World Congress on Formal Methods","author":"Souyris","year":"2009"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2020,12,14]],"date-time":"2020-12-14T04:40:45Z","timestamp":1607920845000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2012.03745v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,3]]},"references-count":22,"URL":"https:\/\/doi.org\/10.4204\/eptcs.329.3","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12,3]]}}}