{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T04:02:59Z","timestamp":1763179379475,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031067723"},{"type":"electronic","value":"9783031067730"}],"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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-06773-0_1","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T11:24:44Z","timestamp":1652959484000},"page":"3-13","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formal Methods for\u00a0Trusted Space Autonomy: Boon or\u00a0Bane?"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1023-9480","authenticated-orcid":false,"given":"Steve A.","family":"Chien","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Agrawal, J., Chi, W., Chien, S.A., Rabideau, G., Gaines, D., Kuhn, S.: Analyzing the effectiveness of rescheduling and flexible execution methods to address uncertainty in execution duration for a planetary rover. Robot. Auton. Syst. 140 (2021) 103758 (2021). https:\/\/doi.org\/10.1016\/j.robot.2021.103758","DOI":"10.1016\/j.robot.2021.103758"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Agrawal, J., et al.: Enabling limited resource-bounded disjunction in scheduling. J. Aerosp. Inf. Syst. 18(6), 322\u2013332 (2021). https:\/\/doi.org\/10.2514\/1.I010908","DOI":"10.2514\/1.I010908"},{"key":"1_CR3","unstructured":"Agrawal, J., Yelamanchili, A., Chien, S.: Using explainable scheduling for the mars 2020 rover mission. In: Workshop on Explainable AI Planning (XAIP), International Conference on Automated Planning and Scheduling (ICAPS XAIP), October 2020. https:\/\/arxiv.org\/pdf\/2011.08733.pdf"},{"key":"1_CR4","unstructured":"Bernard, D.E., et al.: The remote agent experiment. In: Deep Space One Technology Validation Symposium, Pasadena, CA, February 1999. https:\/\/ntrs.nasa.gov\/api\/citations\/20000116204\/downloads\/20000116204.pdf"},{"issue":"5\u20136","key":"1_CR5","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/s00138-007-0081-3","volume":"19","author":"A Castano","year":"2008","unstructured":"Castano, A., et al.: Automatic detection of dust devils and clouds at mars. Mach. Vis. Appl. 19(5\u20136), 467\u2013482 (2008)","journal-title":"Mach. Vis. Appl."},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MS.1987.231415","volume":"4","author":"J Cavano","year":"1987","unstructured":"Cavano, J., LaMonica, F.: Quality assurance in future development environments. IEEE Softw. 4, 26\u201334 (1987)","journal-title":"IEEE Softw."},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Chien, S., et al.: Onboard autonomy on the intelligent payload experiment (IPEX) CubeSat mission. J. Aerosp. Inf. Syst. (JAIS) 14(6), 307\u2013315 (2016). https:\/\/doi.org\/10.2514\/1.I010386","DOI":"10.2514\/1.I010386"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Chien, S., Mclaren, D., Tran, D., Davies, A.G., Doubleday, J., Mandl, D.: Onboard product generation on earth observing one: a pathfinder for the proposed Hyspiri mission intelligent payload module. IEEE JSTARS Special Issue on the Earth Observing One (EO-1) Satellite Mission: Over a decade in space (2013)","DOI":"10.1109\/JSTARS.2013.2249574"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"196","DOI":"10.2514\/1.12923","volume":"2","author":"S Chien","year":"2005","unstructured":"Chien, S., et al.: Using autonomy flight software to improve science return on earth observing one. J. Aerosp. Comput. Inf. Commun. (JACIC) 2, 196\u2013216 (2005)","journal-title":"J. Aerosp. Comput. Inf. Commun. (JACIC)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Chien, S., Wagstaff, K.L.: Robotic space exploration agents. Sci. Robot. (2017). https:\/\/www.science.org\/doi\/10.1126\/scirobotics.aan4831","DOI":"10.1126\/scirobotics.aan4831"},{"key":"1_CR11","unstructured":"Cichy, B., Chien, S., Schaffer, S., Tran, D., Rabideau, G., Sherwood, R.: Validating the autonomous EO-1 science agent. In: International Workshop on Planning and Scheduling for Space (IWPSS 2004), Darmstadt, Germany, June 2004"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Estlin, T., et al.: AEGIS automated targeting for the MER opportunity rover. ACM Trans. Intell. Syst. Technol. 3(3), 1\u201319 (2012). Article No.: 50. https:\/\/doi.org\/10.1145\/2168752.2168764","DOI":"10.1145\/2168752.2168764"},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1023\/A:1008711707946","volume":"8","author":"MS Feather","year":"2001","unstructured":"Feather, M.S., Smith, B.: Automatic generation of test oracles\u2013from pilot studies to application. Autom. Softw. Eng. 8(1), 31\u201361 (2001)","journal-title":"Autom. Softw. Eng."},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Francis, R., et al.: AEGIS autonomous targeting for ChemCam on Mars Science Laboratory: deployment and results of initial science team use. Sci. Robot. 2 (2017). https:\/\/doi.org\/10.1126\/scirobotics.aan4582","DOI":"10.1126\/scirobotics.aan4582"},{"key":"1_CR15","unstructured":"Gaines, D., Rabideau, G., Wong, V., Kuhn, S., Fosse, E., Chien, S.: The Mars 2020 on-board planner: balancing performance and computational constraints. In: Flight Software Workshop, February 2022"},{"key":"1_CR16","unstructured":"George, A.: Margaret Hamilton led the NASA software team that landed astronauts on the moon (2019). https:\/\/www.smithsonianmag.com\/smithsonian-institution\/margaret-hamilton-led-nasa-software-team-landed-astronauts-moon-180971575\/. Accessed 25 Mar 2022"},{"key":"1_CR17","unstructured":"Havelund, K., et al.: Formal analysis of the remote agent before and after flight. In: Lfm 2000: Fifth NASA Langley Formal Methods Workshop (2000)"},{"issue":"8","key":"1_CR18","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K Havelund","year":"2001","unstructured":"Havelund, K., Lowry, M., Penix, J.: Formal analysis of a space-craft controller using spin. IEEE Trans. Softw. Eng. 27(8), 749\u2013765 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Hayden, S.C., Sweet, A.J., Christa, S.E.: Livingstone model-based diagnosis of earth observing one. In: AIAA Intelligent Systems Technical Conference. AIAA (2004). https:\/\/doi.org\/10.2514\/6.2004-6225","DOI":"10.2514\/6.2004-6225"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Hayden, S.C., Sweet, A.J., Shulman, S.: Lessons learned in the livingstone 2 on earth observing one flight experiment. In: AIAA Infotech@Aerospace. AIAA (2005). https:\/\/doi.org\/10.2514\/6.2005-7000","DOI":"10.2514\/6.2005-7000"},{"issue":"2","key":"1_CR21","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2560217.2560218","volume":"57","author":"GJ Holzmann","year":"2014","unstructured":"Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64\u201373 (2014)","journal-title":"Commun. ACM"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-49122-5_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"GJ Holzmann","year":"2016","unstructured":"Holzmann, G.J.: Cloud-based verification of concurrent software. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 311\u2013327. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_15"},{"issue":"4","key":"1_CR23","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/MS.2020.2986107","volume":"37","author":"GJ Holzmann","year":"2020","unstructured":"Holzmann, G.J.: Test fatigue. IEEE Softw. 37(4), 11\u201316 (2020)","journal-title":"IEEE Softw."},{"issue":"6","key":"1_CR24","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/TSE.2010.110","volume":"37","author":"GJ Holzmann","year":"2010","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845\u2013857 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR25","volume-title":"Applied Software Measurement","author":"C Jones","year":"1991","unstructured":"Jones, C.: Applied Software Measurement. McGraw-Hill, New York (1991)"},{"key":"1_CR26","unstructured":"Joyce, E.: Is error free software possible? Datamation 35(18), 749\u2013765 (1989)"},{"key":"1_CR27","unstructured":"JPL-Artificial-Intelligence-Group: Autonomous sciencecraft web site (2017). https:\/\/ai.jpl.nasa.gov\/public\/projects\/ase\/. Accessed 25 Mar 2022"},{"key":"1_CR28","unstructured":"JPL-Artificial-Intelligence-Group: Mars 2020 onboard planner web site (2017). https:\/\/ai.jpl.nasa.gov\/public\/projects\/m2020-scheduler\/. Accessed 25 Mar 2022"},{"key":"1_CR29","volume-title":"Software Reliability: Measurement, Prediction, Application","author":"J Musa","year":"1990","unstructured":"Musa, J., et al.: Software Reliability: Measurement, Prediction, Application. McGraw-Hill, New York (1990)"},{"issue":"1\u20132","key":"1_CR30","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0004-3702(98)00068-X","volume":"103","author":"N Muscettola","year":"1998","unstructured":"Muscettola, N., Nayak, P.P., Pell, B., Williams, B.C.: Remote agent: to boldly go where no AI system has gone before. Artif. Intell. 103(1\u20132), 5\u201347 (1998)","journal-title":"Artif. Intell."},{"key":"1_CR31","unstructured":"NASA: Chapter two: Computers on board the apollo spacecraft. In: Computers in Spaceflight: The NASA Experience. NASA. https:\/\/history.nasa.gov\/computers\/Ch2-6.html?mod=article_inline. Accessed 27 Mar 2022"},{"key":"1_CR32","unstructured":"Rabideau, G., et al.: Onboard automated scheduling for the Mars 2020 rover. In: Proceedings of the International Symposium on Artificial Intelligence, Robotics and Automation for Space, i-SAIRAS 2020, European Space Agency, Noordwijk, NL (2020)"},{"key":"1_CR33","unstructured":"Smith, B.D., Feather, M.S., Muscettola, N.: Challenges and methods in testing the remote agent planner. In: AIPS, pp. 254\u2013263 (2000)"},{"key":"1_CR34","unstructured":"Tran, D., Chien, S., Rabideau, G., Cichy, B.: Flight software issues in onboard automated planning: Lessons learned on EO-1. In: International Workshop on Planning and Scheduling for Space (IWPSS 2004), Darmstadt, Germany, June 2004. https:\/\/ai.jpl.nasa.gov\/public\/papers\/tran_iwpss2004.pdf"},{"key":"1_CR35","unstructured":"Tran, D., Chien, S., Rabideau, G., Cichy, B.: Safe agents in space: preventing and responding to anomalies in the autonomous sciencecraft experiment. In: Safety and Security in Multi Agent Systems Workshop (SASEMAS), Autonomous Agents and Multi-Agent Systems Conference (AAMAS 2005), Utrecht, Netherlands, July 2005. https:\/\/ai.jpl.nasa.gov\/public\/papers\/tran_sasemas2005_PreventingResponding.pdf"},{"key":"1_CR36","unstructured":"Yelamanchili, A., et al.: Ground-based automated scheduling for operations of the Mars 2020 rover mission. In: Proceedings Space Operations 2021, May 2021. https:\/\/spaceops.iafastro.directory\/a\/proceedings\/SpaceOps-2021\/SpaceOps-2021\/6\/manuscripts\/SpaceOps-2021,6,x1385.pdf"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-06773-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T11:07:21Z","timestamp":1659352041000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06773-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067723","9783031067730"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06773-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"20 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, 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":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2022\/","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":"118","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":"33","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":"6","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":"28% - 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":"6.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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}