{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T02:56:46Z","timestamp":1791341806635,"version":"4.3.1"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995232","type":"print"},{"value":"9783030995249","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA\u2019s Formal Requirement Elicitation Tool (<jats:sc>fret<\/jats:sc>), and the RV system<jats:sc>Copilot<\/jats:sc>. We extend<jats:sc>fret<\/jats:sc>with mechanisms to capture additional information needed to generate monitors, and introduce<jats:sc>Ogma<\/jats:sc>, a new tool to bridge the gap between<jats:sc>fret<\/jats:sc>and<jats:sc>Copilot<\/jats:sc>. With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our toolchain is available as open source.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_21","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"387-395","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["Automated Translation of Natural Language Requirements to Runtime Monitors"],"prefix":"10.1007","author":[{"given":"Ivan","family":"Perez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom","family":"Pressburger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alwyn","family":"Goodloe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"21_CR1","unstructured":"Copilot. https:\/\/github.com\/Copilot-Language\/copilot\/. Accessed Oct 04, 2021"},{"key":"21_CR2","unstructured":"FRET: Formal Requirements Elicitation Tool. https:\/\/github.com\/NASA-SW-VnV\/fret\/. Accessed Oct 04, 2021"},{"key":"21_CR3","unstructured":"FRET: Formal Requirements Elicitation Tool - User Manual. https:\/\/github.com\/NASA-SW-VnV\/fret\/blob\/master\/fret-electron\/docs\/_media\/userManual.md. See Section \u201cExporting for Analysis\u201d. Accessed Oct 04, 2021"},{"key":"21_CR4","unstructured":"Ogma. https:\/\/github.com\/nasa\/ogma\/. Accessed Oct 04, 2021"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"E. Bartocci, Y. Falcone, A. Francalanza, and G. Reger. Introduction to runtime verification. In Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science, pages 1\u201333. Springer, 2018","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"J. Baumeister, B. Finkbeiner, S. Schirmer, M. Schwenger, and C. Torens. RTLola cleared for take-off: Monitoring autonomous aircraft. In S. K. Lahiri and C. Wang, editors, Computer Aided Verification, pages 28\u201339, Cham, 2020. Springer International Publishing","DOI":"10.1007\/978-3-030-53291-8_3"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"S. Biewer, B. Finkbeiner, H. Hermanns, M. A. K\u00f6hl, Y. Schnitzer, and M. Schwenger. RTLola on board: Testing real driving emissions on your phone. In J. F. Groote and K. G. Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 365\u2013372, Cham, 2021. Springer International Publishing","DOI":"10.26226\/morressier.604907f41a80aac83ca25ce3"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"A. Boteanu, T. Howard, J. Arkin, and H. Kress-Gazit. A model for verifiable grounding and execution of complex natural language instructions. In 2016 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 2649\u20132654, 2016","DOI":"10.1109\/IROS.2016.7759412"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"K. Claessen and J. Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. ACM Sigplan Notices, 46(4):53\u201364, 2011","DOI":"10.1145\/1988042.1988046"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"D. Cohen, M. S. Feather, K. Narayanaswamy, and S. S. Fickas. Automatic monitoring of software requirements. In Proceedings of the 19th International Conference on Software Engineering, pages 602\u2013603, 1997","DOI":"10.1145\/253228.253493"},{"key":"21_CR11","unstructured":"C. Elliott. On example models and challenges ahead for the evaluation of complex cyber-physical systems with state of the art formal methods V&V, Lockheed Martin Skunk Works. In A. F. R. Laboratory, editor, Safe & Secure Systems and Software Symposium (S5), 2015"},{"key":"21_CR12","unstructured":"C. Elliott. An example set of cyber-physical V&V challenges for S5, Lockheed Martin Skunk Works. In A. F. R. Laboratory, editor, Safe & Secure Systems and Software Symposium (S5), 2016"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"P. Faymonville, B. Finkbeiner, M. Schledjewski, M. Schwenger, M. Stenger, L. Tentrup, and H. Torfah. StreamLAB: Stream-based monitoring of cyber-physical systems. In I. Dillig and S. Tasiran, editors, Computer Aided Verification, pages 421\u2013431, Cham, 2019. Springer International Publishing","DOI":"10.1007\/978-3-030-25540-4_24"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"A. Fifarek, L. G. Wagner, J. A. Hoffman, B. D. Rodes, M. A. Aiello, and J. A. Davis. SpeAR v2.0: Formalized past LTL specification and analysis of requirements. In NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16\u201318, 2017, Proceedings, pages 420\u2013426, 2017","DOI":"10.1007\/978-3-319-57288-8_30"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"A. Gacek, J. Backes, M. Whalen, L. Wagner, and E. Ghassabani. The jk ind model checker. In International Conference on Computer Aided Verification, pages 20\u201327. Springer, 2018","DOI":"10.1007\/978-3-319-96142-2_3"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"S. Ghosh, D. Elenius, W. Li, P. Lincoln, N. Shankar, and W. Steiner. ARSENAL: automatic requirements specification extraction from natural language. In S. Rayadurgam and O. Tkachuk, editors, NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings, volume 9690 of Lecture Notes in Computer Science, pages 41\u201346. Springer, 2016","DOI":"10.1007\/978-3-319-40648-0_4"},{"key":"21_CR17","unstructured":"D. Giannakopoulou, T. Pressburger, A. Mavridou, J. Rhein, J. Schumann, and N. Shi. Formal requirements elicitation with FRET. In 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), 2020"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"D. Giannakopoulou, T. Pressburger, A. Mavridou, and J. Schumann. Automated formalization of structured natural language requirements. Inf. Softw. Technol., 137:106590, 2021","DOI":"10.1016\/j.infsof.2021.106590"},{"key":"21_CR19","unstructured":"A. Goodloe and L. Pike. Monitoring distributed real-time systems: A survey and future directions. Technical Report NASA\/CR-2010-216724, NASA Langley Research Center, July 2010"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data flow programming language LUSTRE. Proceedings of the IEEE, 79(9):1305\u20131320, 1991","DOI":"10.1109\/5.97300"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"K. Havelund and A. Goldberg. Verify Your Runs, pages 374\u2013383. Springer, Berlin Heidelberg, Berlin, Heidelberg, 2008","DOI":"10.1007\/978-3-540-69149-5_40"},{"key":"21_CR22","unstructured":"B. Jeannet and F. Gaucher. Debugging embedded systems requirements with STIMULUS: an automotive case-study. In 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016), Toulouse, France, Jan. 2016"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"J. C. Knight. Safety critical systems: Challenges and directions. In Proceedings of the 24th International Conference on Software Engineering, ICSE \u201902, pages 547\u2013550. ACM, 2002","DOI":"10.1145\/581339.581406"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"C. Lignos, V. Raman, C. Finucane, M. Marcus, and H. Kress-Gazit. Provably correct reactive control from natural language. Auton. Robots, 38(1):89\u2013105, jan 2015","DOI":"10.1007\/s10514-014-9418-8"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"L. L\u00facio, S. Rahman, C.-H. Cheng, and A. Mavin. Just formal enough? Automated analysis of EARS requirements. In NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings, pages 427\u2013434, May 2017","DOI":"10.1007\/978-3-319-57288-8_31"},{"key":"21_CR26","unstructured":"A. Mavridou, H. Bourbouh, P. L. Garoche, and M. Hejase. Evaluation of the FRET and CoCoSim tools on the ten Lockheed Martin cyber-physical challenge problems. Technical Report TM-2019-220374, National Aeronautics and Space Administration, February 2020"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"A. Mavridou, H. Bourbouh, D. Giannakopoulou, T. Pressburger, M. Hejase, P.-L. Garoche, and J. Schumann. The ten Lockheed Martin cyber-physical challenges: Formalized, analyzed, and explained. In 2020 IEEE 28th International Requirements Engineering Conference (RE), pages 300\u2013310, 2020","DOI":"10.1109\/RE48521.2020.00040"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"P. Moosbrugger, K. Y. Rozier, and J. Schumann. R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. Formal Methods in System Design, 51(1):31\u201361, 2017","DOI":"10.1007\/s10703-017-0275-x"},{"key":"21_CR29","unstructured":"I. Perez, F. Dedden, and A. Goodloe. Copilot 3. Technical Report NASA\/TM\u20132020\u2013220587, NASA Langley Research Center, April 2020"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"I. Perez, A. Goodloe, and W. Edmonson. Fault-tolerant swarms. In 2019 IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT), pages 47\u201354. IEEE, 2019","DOI":"10.1109\/SMC-IT.2019.00011"},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"I. Perez and A. E. Goodloe. Fault-tolerant functional reactive programming (extended version). Journal of Functional Programming, 30, 2020","DOI":"10.1017\/S0956796820000118"},{"key":"21_CR32","unstructured":"I. Perez, A. Mavridou, T. Pressburger, A. Goodloe, and D. Giannakopoulou. Artifact for Automated Translation of Natural Language Requirements to Runtime Monitors. https:\/\/doi.org\/10.5281\/zenodo.5888956. Accessed Jan 21, 2022"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"I. Perez, A. Mavridou, T. Pressburger, A. Goodloe, and D. Giannakopoulou. Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors. Technical Report NASA\/TM\u201320220000049, NASA, January 2022","DOI":"10.1007\/978-3-030-99524-9_21"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"I. Perez and H. Nilsson. Runtime verification and validation of functional reactive systems. Journal of Functional Programming, 30:e28, 2020","DOI":"10.1017\/S0956796820000210"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"L. Pike, A. Goodloe, R. Morisset, and S. Niller. Copilot: A hard real-time runtime monitor. In Proceedings of the 1st Intl. Conference on Runtime Verification, LNCS. Springer, November 2010","DOI":"10.1007\/978-3-642-16612-9_26"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"L. Pike, N. Wegmann, S. Niller, and A. Goodloe. Copilot: Monitoring embedded systems. Innov. Syst. Softw. Eng., 9(4):235\u2013255, Dec. 2013","DOI":"10.1007\/s11334-013-0223-x"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"T. Reinbacher, K. Y. Rozier, and J. Schumann. Temporal-logic based runtime observer pairs for system health management of real-time systems. In E. \u00c1brah\u00e1m and K. Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 357\u2013372, Berlin, Heidelberg, 2014. Springer, Berlin Heidelberg","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"J. Schumann, P. Moosbrugger, and K. Y. Rozier. R2u2: monitoring and diagnosis of security threats for unmanned aerial systems. In Runtime Verification, pages 233\u2013249. Springer, 2015","DOI":"10.1007\/978-3-319-23820-3_15"},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"H. Torfah. Stream-based monitors for real-time properties. In B. Finkbeiner and L. Mariani, editors, Runtime Verification - 19th International Conference, RV 2019, Porto, Portugal, October 8-11, 2019, Proceedings, volume 11757 of Lecture Notes in Computer Science, pages 91\u2013110. Springer, 2019","DOI":"10.1007\/978-3-030-32079-9_6"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"J. Wilmot. A core flight software system. In Proceedings of the 3rd IEEE\/ACM\/IFIP International Conference on Hardware\/Software Codesign and System Synthesis, CODES+ISSS \u201905, pages 13\u201314, New York, NY, USA, 2005. ACM","DOI":"10.1145\/1084834.1084842"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T17:04:17Z","timestamp":1675098257000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}