{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:21:17Z","timestamp":1743124877041,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030605070"},{"type":"electronic","value":"9783030605087"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-60508-7_12","type":"book-chapter","created":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T04:33:06Z","timestamp":1602045186000},"page":"221-240","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Actor-Based Runtime Verification with MESA"],"prefix":"10.1007","author":[{"given":"Nastaran","family":"Shafiei","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Mehlitz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,10,2]]},"reference":[{"key":"12_CR1","unstructured":"Akka (2020). http:\/\/doc.akka.io\/docs\/akka\/current\/scala.html"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-25423-4_1","volume-title":"Formal Methods and Software Engineering","author":"C Artho","year":"2015","unstructured":"Artho, C., Havelund, K., Kumar, R., Yamagata, Y.: Domain-specific languages with scala. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 1\u201316. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_1"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-66197-1_14","volume-title":"Software Engineering and Formal Methods","author":"DP Attard","year":"2017","unstructured":"Attard, D.P., Francalanza, A.: Trace partitioning and local monitoring for asynchronous components. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 219\u2013235. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_14"},{"key":"12_CR4","unstructured":"Avrekh, I., Matthews, B.L., Stewart, M.: RNAV adherence data integration system using aviation and environmental sources. Technical report, NASA Ames Research Center, June 2018"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-35632-2_20","volume-title":"Runtime Verification","author":"B Barre","year":"2013","unstructured":"Barre, B., Klein, M., Soucy-Boivin, M., Ollivier, P.-A., Hall\u00e9, S.: MapReduce for parallel trace validation of LTL properties. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 184\u2013198. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_20"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-21437-0_7","volume-title":"FM 2011: Formal Methods","author":"H Barringer","year":"2011","unstructured":"Barringer, H., Havelund, K.: TraceContract: a scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57\u201372. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_7"},{"key":"12_CR7","unstructured":"Barringer, H., Havelund, K., Kurklu, E., Morris, R.: Checking flight rules with tracecontract: application of a scala DSL for trace analysis. Technical report, Jet Propulsion Laboratory, National Aeronautics and Space Administration, Pasadena, CA, USA (2011). http:\/\/hdl.handle.net\/2014\/42194"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/s10703-016-0242-y","volume":"49","author":"D Basin","year":"2016","unstructured":"Basin, D., Caronni, G., Ereth, S., Harvan, M., Klaedtke, F., Mantel, H.: Scalable offline monitoring of temporal specification. Formal Methods Syst. Des. 49, 75\u2013108 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0242-y","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"12_CR9","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10703-015-0226-3","volume":"46","author":"S Berkovich","year":"2015","unstructured":"Berkovich, S., Bonakdarpour, B., Fischmeister, S.: Runtime verification with minimal intrusion through parallelism. Formal Methods Syst. Des. 46(3), 317\u2013348 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0226-3","journal-title":"Formal Methods Syst. Des."},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-030-50086-3_13","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"C Bartolo Burl\u00f2","year":"2020","unstructured":"Bartolo Burl\u00f2, C., Francalanza, A., Scalas, A.: Towards a hybrid verification methodology for communication protocols (short paper). In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 227\u2013235. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_13"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-33826-7_15","volume-title":"Software Engineering and Formal Methods","author":"C Colombo","year":"2012","unstructured":"Colombo, C., Francalanza, A., Mizzi, R., Pace, G.J.: polyLarva: runtime verification with configurable resource-aware monitoring boundaries. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 218\u2013232. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_15"},{"key":"12_CR12","unstructured":"Department of Transportation, Federal Aviation Administration: Implementation of Descend Via into Boston Terminal area from Boston ARTCC (2015)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-030-03769-7_6","volume-title":"Runtime Verification","author":"A El-Hokayem","year":"2018","unstructured":"El-Hokayem, A., Falcone, Y.: Can we monitor all multithreaded programs? In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 64\u201389. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_6"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D., Kalus, G. (eds.) Engineering Dependable Software Systems, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 34, pp. 141\u2013175. IOS Press, January 2013. https:\/\/doi.org\/10.3233\/978-1-61499-207-3-141","DOI":"10.3233\/978-1-61499-207-3-141"},{"key":"12_CR15","unstructured":"SWIM Flight Data Publication Service (2020). https:\/\/www.faa.gov\/air_traffic\/technology\/swim\/sfdps\/"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-75632-5_6","volume-title":"Lectures on Runtime Verification","author":"A Francalanza","year":"2018","unstructured":"Francalanza, A., P\u00e9rez, J.A., S\u00e1nchez, C.: Runtime verification for decentralised and distributed systems. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 176\u2013210. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_6"},{"issue":"3","key":"12_CR17","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/s10703-014-0217-9","volume":"46","author":"A Francalanza","year":"2014","unstructured":"Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Methods Syst. Des. 46(3), 226\u2013261 (2014). https:\/\/doi.org\/10.1007\/s10703-014-0217-9","journal-title":"Formal Methods Syst. Des."},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-319-67531-2_22","volume-title":"Runtime Verification","author":"S Hall\u00e9","year":"2017","unstructured":"Hall\u00e9, S., Khoury, R., Gaboury, S.: Event stream processing with multiple threads. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 359\u2013369. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67531-2_22"},{"key":"12_CR19","unstructured":"Harris Corporation: FAA Telecommunications Infrastructure NEMS User Guide (2013)"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Havelund, K.: Data automata in scala. In: Symposium on Theoretical Aspects of Software Engineering Conference, pp. 1\u20139. Changsha, China (2014). https:\/\/doi.org\/10.1109\/TASE.2014.37","DOI":"10.1109\/TASE.2014.37"},{"key":"12_CR21","unstructured":"Havelund, K.: Daut (2020). https:\/\/github.com\/havelund\/daut"},{"key":"12_CR22","unstructured":"Havelund, K.: TraceContract (2020). https:\/\/github.com\/havelund\/tracecontract"},{"key":"12_CR23","unstructured":"Hewitt, C., Bishop, P., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pp. 235\u2013245. Morgan Kaufmann Publishers Inc., San Francisco (1973)"},{"key":"12_CR24","unstructured":"International Air Line Pilots Associations: FAA Suspends OPD Arrivals for Atlanta International Airport (2016)"},{"key":"12_CR25","unstructured":"International Civil Aviation Organization (ICAO): Performance-based Navigation (PBN) Manual, 3 edn., May 2008"},{"key":"12_CR26","unstructured":"JMH - Java Microbenchmark Harness (2020). https:\/\/openjdk.java.net\/projects\/code-tools\/jmh\/"},{"issue":"2","key":"12_CR27","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1145\/13677.22723","volume":"5","author":"J Joyce","year":"1987","unstructured":"Joyce, J., Lomow, G., Slind, K., Unger, B.: Monitoring distributed systems. ACM Trans. Comput. Syst. 5(2), 121\u2013150 (1987). https:\/\/doi.org\/10.1145\/13677.22723","journal-title":"ACM Trans. Comput. Syst."},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Lavery, P., Watanabe, T.: An actor-based runtime monitoring system for web and desktop applications. In: Hochin, T., Hirata, H., Nomiya, H. (eds.) International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel\/Distributed Computing, pp. 385\u2013390. IEEE Computer Society (2017)","DOI":"10.1109\/SNPD.2017.8022750"},{"issue":"5","key":"12_CR29","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293\u2013303 (2009). https:\/\/doi.org\/10.1016\/j.jlap.2008.08.004","journal-title":"J. Logic Algebraic Program."},{"key":"12_CR30","unstructured":"Mehlitz, P.: RACE (2020) http:\/\/nasarace.github.io\/race\/"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Mehlitz, P., Shafiei, N., Tkachuk, O., Davies, M.: RACE: building airspace simulations faster and better with actors. In: Digital Avionics Systems Conference (DASC), pp. 1\u20139, September 2016. https:\/\/doi.org\/10.1109\/DASC.2016.7777991","DOI":"10.1109\/DASC.2016.7777991"},{"key":"12_CR32","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2011","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Ro\u015fu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tech. Technol. Transf. 14, 249\u2013289 (2011). https:\/\/doi.org\/10.1007\/s10009-011-0198-6","journal-title":"Int. J. Softw. Tech. Technol. Transf."},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: Wu, P., Hack, S. (eds.) International Conference on Compiler Construction, pp. 98\u2013108. ACM (2017). https:\/\/doi.org\/10.1145\/3033019.3033031","DOI":"10.1145\/3033019.3033031"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Rasmussen, S., Kingston, D., Humphrey, L.: A brief introduction to unmanned systems autonomy services (UxAS). In: 2018 International Conference on Unmanned Aircraft Systems (ICUAS), pp. 257\u2013268 (2018). https:\/\/doi.org\/10.1109\/ICUAS.2018.8453287","DOI":"10.1109\/ICUAS.2018.8453287"},{"key":"12_CR35","unstructured":"Reger, G.: Rule-Based Runtime Verification in a Multicore System Setting. Master\u2019s thesis, University of Manchester (2010)"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/978-3-662-46681-0_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Reger","year":"2015","unstructured":"Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 596\u2013610. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_55"},{"key":"12_CR37","volume-title":"Java Message Service","author":"M Richards","year":"2009","unstructured":"Richards, M., Monson-Haefel, R., Chappell, D.A.: Java Message Service, 2nd edn. O\u2019Reilly Media Inc., Newton (2009)","edition":"2"},{"key":"12_CR38","volume-title":"Akka in Action","author":"R Roestenburg","year":"2015","unstructured":"Roestenburg, R., Bakker, R., Williams, R.: Akka in Action, 1st edn. Manning Publications Co., Greenwich (2015)","edition":"1"},{"key":"12_CR39","doi-asserted-by":"crossref","unstructured":"Shafiei, N., Havelund, K., Mehlitz, P.: Empirical study of actor-based runtime verification. Technical report, NASA Ames Research Center, June 2020","DOI":"10.1007\/978-3-030-60508-7_12"},{"key":"12_CR40","doi-asserted-by":"crossref","unstructured":"Stewart, M., Matthews, B.: Objective assessment method for RNAV STAR adherence. In: DASC: Digital Avionics Systems Conference (2017)","DOI":"10.1109\/DASC.2017.8102034"},{"key":"12_CR41","unstructured":"U.S. Department of Transportation. Federal Aviation Administration: Performance Based Navigation PBN NAS Navigation Strategy (2016)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-60508-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T12:56:44Z","timestamp":1619269004000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-60508-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030605070","9783030605087"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-60508-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"2 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv20.ait.ac.at\/","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":"43","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":"14","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":"2","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":"33% - 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.95","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":"3.82","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":"Also accepted and included: an invited paper, 5 tutorial, 6 tool papers, and a benchmark paper. The conference was held virtually due to the COVID-19 pandemic.","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)"}}]}}