{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T02:42:49Z","timestamp":1772505769482,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030576271","type":"print"},{"value":"9783030576288","type":"electronic"}],"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-57628-8_12","type":"book-chapter","created":{"date-parts":[[2020,8,24]],"date-time":"2020-08-24T23:19:22Z","timestamp":1598311162000},"page":"196-214","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2239-4218","authenticated-orcid":false,"given":"Brian","family":"Kempa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9560-2175","authenticated-orcid":false,"given":"Pei","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8220-7552","authenticated-orcid":false,"given":"Phillip H.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0566-5744","authenticated-orcid":false,"given":"Joseph","family":"Zambreno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,8,25]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-11900-7_18","volume-title":"Simulation, Modeling, and Programming for Autonomous Robots","author":"S Adam","year":"2014","unstructured":"Adam, S., Larsen, M., Jensen, K., Schultz, U.P.: Towards rule-based dynamic safety monitoring for mobile robots. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds.) SIMPAR 2014. LNCS (LNAI), vol. 8810, pp. 207\u2013218. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11900-7_18"},{"issue":"1","key":"12_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35\u201377 (1993)","journal-title":"Inf. Comput."},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Badger, J., Hulse, A., Taylor, R., Curtis, A., Gooding, D., Thackston, A.: Model-based robotic dynamic motion control for the Robonaut 2 humanoid robot. In: 2013 13th IEEE-RAS International Conference on Humanoid Robots (Humanoids), pp. 62\u201367, October 2013. https:\/\/doi.org\/10.1109\/HUMANOIDS.2013.7029956","DOI":"10.1109\/HUMANOIDS.2013.7029956"},{"key":"12_CR4","series-title":"Studies in Computational Intelligence","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-26054-9_13","volume-title":"Robot Operating System (ROS)","author":"J Badger","year":"2016","unstructured":"Badger, J., Gooding, D., Ensley, K., Hambuchen, K., Thackston, A.: ROS in space: a case study on Robonaut 2. In: Koubaa, A. (ed.) Robot Operating System (ROS). SCI, vol. 625, pp. 343\u2013373. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-26054-9_13"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Clemens, J., Pal, R., Sherrell, B.: Runtime state verification on resource-constrained platforms. In: MILCOM 2018\u20132018 IEEE Military Communications Conference (MILCOM), pp. 1\u20136. IEEE (2018)","DOI":"10.1109\/MILCOM.2018.8599862"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Cooper, K., Eckhardt, J., Kennedy, K.: Redundancy elimination revisited. In: Proceedings of the 17th International Conference on Parallel Architectures and Compilation Techniques, pp. 12\u201321. ACM (2008)","DOI":"10.1145\/1454115.1454120"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Cowley, A., Taylor, C.J.: Towards language-based verification of robot behaviors. In: 2011 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 4776\u20134782. IEEE (2011)","DOI":"10.1109\/IROS.2011.6095028"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Diftler, M.A., et al.: Robonaut 2 - the first humanoid robot in space. In: 2011 IEEE International Conference on Robotics and Automation, pp. 2178\u20132183, May 2011. https:\/\/doi.org\/10.1109\/ICRA.2011.5979830","DOI":"10.1109\/ICRA.2011.5979830"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-11164-3_18","volume-title":"Runtime Verification","author":"J Geist","year":"2014","unstructured":"Geist, J., Rozier, K.Y., Schumann, J.: Runtime observer pairs and Bayesian network reasoners on-board FPGAs: flight-certifiable system health management for embedded systems. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 215\u2013230. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_18"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Halder, R., Proen\u00e7a, J., Macedo, N., Santos, A.: Formal verification of ROS-based robotic applications using timed-automata. In: 2017 IEEE\/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 44\u201350. IEEE (2017)","DOI":"10.1109\/FormaliSE.2017.9"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-11164-3_20","volume-title":"Runtime Verification","author":"J Huang","year":"2014","unstructured":"Huang, J., et al.: ROSRV: runtime verification for robots. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 247\u2013254. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_20"},{"key":"12_CR12","unstructured":"Badger, J.M., Hulse, A.M., Thackston, A.: Advancing safe human-robot interactions with Robonaut 2. In: Proceedings of the 12th International Symposium on Artificial Intelligence, Robotics and Automation in Space (2014)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-23820-3_7","volume-title":"Runtime Verification","author":"A Kane","year":"2015","unstructured":"Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 102\u2013117. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_7"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-25543-5_1","volume-title":"Computer Aided Verification","author":"J Li","year":"2019","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 3\u201322. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_1"},{"key":"12_CR15","unstructured":"Lu, H., Forin, A.: The design and implementation of p2v, an architecture for zero-overhead online verification of software programs. Technical report MSR-TR-2007-99, Microsoft Research, August 2007"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Luckcuck, M., Farrell, M., Dennis, L., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. arXiv preprint arXiv:1807.00048 (2018)","DOI":"10.1145\/3342355"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Mukherjee, R., Purandare, M., Polig, R., Kroening, D.: Formal techniques for effective co-verification of hardware\/software co-designs. In: Proceedings of the 54th Annual Design Automation Conference 2017, p. 35. ACM (2017)","DOI":"10.1145\/3061639.3062253"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Pellizzoni, R., Meredith, P., Caccamo, M., Rosu, G.: Hardware runtime monitoring for dependable cots-based real-time embedded systems. In: 2008 Real-Time Systems Symposium, pp. 481\u2013491, November 2008","DOI":"10.1109\/RTSS.2008.43"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Pratt, G.A., Williamson, M.M.: Series elastic actuators. In: Proceedings 1995 IEEE\/RSJ International Conference on Intelligent Robots and Systems. Human Robot Interaction and Cooperative Robots, vol. 1, pp. 399\u2013406, August 1995. https:\/\/doi.org\/10.1109\/IROS.1995.525827","DOI":"10.1109\/IROS.1995.525827"},{"key":"12_CR20","unstructured":"Quigley, M., et al.: ROS: an open-source robot operating system. In: ICRA Workshop on Open Source Software, vol. 3, p. 5. Kobe, Japan (2009)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-54862-8_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357\u2013372. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_24"},{"key":"12_CR22","unstructured":"Rozier, K.Y., Schumann, J.: R2U2: tool overview. In: Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES), vol. 3, pp. 138\u2013156. Kalpa Publications, Seattle, September 2017. TBD, https:\/\/easychair.org\/publications\/paper\/Vncw"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Rozier, K., Vardi, M.: LTL satisfiability checking. Int. J. Software Tools Technol. Transfer (STTT) 12(2), 123\u2013137 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0140-3","DOI":"10.1007\/s10009-010-0140-3"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-319-23820-3_15","volume-title":"Runtime Verification","author":"J Schumann","year":"2015","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 233\u2013249. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_15"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-319-46982-9_35","volume-title":"Runtime Verification","author":"J Schumann","year":"2016","unstructured":"Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime analysis with R2U2: a tool exhibition report. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 504\u2013509. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_35"},{"issue":"1","key":"12_CR26","first-page":"1","volume":"6","author":"J Schumann","year":"2015","unstructured":"Schumann, J., Rozier, K.Y., Reinbacher, T., Mengshoel, O.J., Mbaya, T., Ippolito, C.: Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. Int. J. Prognost. Health Manage. (IJPHM) 6(1), 1\u201327 (2015)","journal-title":"Int. J. Prognost. Health Manage. (IJPHM)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Solet, D., B\u00e9chennec, J.L., Briday, M., Faucou, S., Pillement, S.: Hardware runtime verification of a RTOS kernel: Evaluation using fault injection. In: 2018 14th European Dependable Computing Conference (EDCC), pp. 25\u201332. IEEE (2018)","DOI":"10.1109\/EDCC.2018.00016"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Wong, L., Arora, N.S., Gao, L., Hoang, T., Wu, J.: Oracle streams: a high performance implementation for near real time asynchronous replication. In: 2009 IEEE 25th International Conference on Data Engineering, pp. 1363\u20131374. IEEE (2009)","DOI":"10.1109\/ICDE.2009.121"},{"key":"12_CR29","unstructured":"Zhang, P., Zambreno, J., Jones, P.H., Rozier, K.: Model predictive runtime verification for embedded platforms with real-time deadlines (2020, Under submission)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-57628-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T11:05:52Z","timestamp":1617707152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-57628-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030576271","9783030576288"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-57628-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"25 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vienna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","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":"1 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"formats2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/formats-2020.cs.ru.nl\/","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":"36","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":"16","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":"0","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":"44% - 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":"3","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":"Due to the Corona pandemic FORMATS 2020 was held as a virtual event.","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)"}}]}}