-
Operations for Autonomous Spacecraft
Authors:
Rebecca Castano,
Tiago Vaquero,
Federico Rossi,
Vandi Verma,
Ellen Van Wyk,
Dan Allard,
Bennett Huffmann,
Erin M. Murphy,
Nihal Dhamani,
Robert A. Hewitt,
Scott Davidoff,
Rashied Amini,
Anthony Barrett,
Julie Castillo-Rogez,
Steve A. Chien,
Mathieu Choukroun,
Alain Dadaian,
Raymond Francis,
Benjamin Gorr,
Mark Hofstadter,
Mitch Ingham,
Cristina Sorice,
Iain Tierney
Abstract:
Onboard autonomy technologies such as planning and scheduling, identification of scientific targets, and content-based data summarization, will lead to exciting new space science missions. However, the challenge of operating missions with such onboard autonomous capabilities has not been studied to a level of detail sufficient for consideration in mission concepts. These autonomy capabilities will…
▽ More
Onboard autonomy technologies such as planning and scheduling, identification of scientific targets, and content-based data summarization, will lead to exciting new space science missions. However, the challenge of operating missions with such onboard autonomous capabilities has not been studied to a level of detail sufficient for consideration in mission concepts. These autonomy capabilities will require changes to current operations processes, practices, and tools. We have developed a case study to assess the changes needed to enable operators and scientists to operate an autonomous spacecraft by facilitating a common model between the ground personnel and the onboard algorithms. We assess the new operations tools and workflows necessary to enable operators and scientists to convey their desired intent to the spacecraft, and to be able to reconstruct and explain the decisions made onboard and the state of the spacecraft. Mock-ups of these tools were used in a user study to understand the effectiveness of the processes and tools in enabling a shared framework of understanding, and in the ability of the operators and scientists to effectively achieve mission science objectives.
△ Less
Submitted 21 November, 2021;
originally announced November 2021.
-
Advancing the Scientific Frontier with Increasingly Autonomous Systems
Authors:
Rashied Amini,
Abigail Azari,
Shyam Bhaskaran,
Patricia Beauchamp,
Julie Castillo-Rogez,
Rebecca Castano,
Seung Chung,
John Day,
Richard Doyle,
Martin Feather,
Lorraine Fesq,
Jeremy Frank,
P. Michael Furlong,
Michel Ingham,
Brian Kennedy,
Ksenia Kolcio,
Issa Nesnas,
Robert Rasmussen,
Glenn Reeves,
Cristina Sorice,
Bethany Theiling,
Jay Wyatt
Abstract:
A close partnership between people and partially autonomous machines has enabled decades of space exploration. But to further expand our horizons, our systems must become more capable. Increasing the nature and degree of autonomy - allowing our systems to make and act on their own decisions as directed by mission teams - enables new science capabilities and enhances science return. The 2011 Planet…
▽ More
A close partnership between people and partially autonomous machines has enabled decades of space exploration. But to further expand our horizons, our systems must become more capable. Increasing the nature and degree of autonomy - allowing our systems to make and act on their own decisions as directed by mission teams - enables new science capabilities and enhances science return. The 2011 Planetary Science Decadal Survey (PSDS) and on-going pre-Decadal mission studies have identified increased autonomy as a core technology required for future missions. However, even as scientific discovery has necessitated the development of autonomous systems and past flight demonstrations have been successful, institutional barriers have limited its maturation and infusion on existing planetary missions. Consequently, the authors and endorsers of this paper recommend that new programmatic pathways be developed to infuse autonomy, infrastructure for support autonomous systems be invested in, new practices be adopted, and the cost-saving value of autonomy for operations be studied.
△ Less
Submitted 15 September, 2020;
originally announced September 2020.
-
Verification Coverage
Authors:
Rodrigo Castaño,
Victor Braberman,
Diego Garbervetsky,
Sebastian Uchitel
Abstract:
Software Model Checkers have shown outstanding performance improvements in recent times. Moreover, for specific use cases, formal verification techniques have shown to be highly effective, leading to a number of high-profile success stories. However, widespread adoption remains unlikely in the short term and one of the remaining obstacles in that direction is the vast number of instances which sof…
▽ More
Software Model Checkers have shown outstanding performance improvements in recent times. Moreover, for specific use cases, formal verification techniques have shown to be highly effective, leading to a number of high-profile success stories. However, widespread adoption remains unlikely in the short term and one of the remaining obstacles in that direction is the vast number of instances which software model checkers cannot fully analyze within reasonable memory and CPU bounds. The majority of verification tools fail to provide a measure of progress or any intermediate verification result when such situations occur.
Inspired in the success that coverage metrics have achieved in industry, we propose to adapt the definition of coverage to the context of verification. We discuss some of the challenges in pinning down a definition that resembles the deeply rooted semantics of test coverage. Subsequently we propose a definition for a broad family of verification techniques: those based on Abstract Reachability Trees. Moreover, we discuss a general approach to computing an under-approximation of such metric and a specific heuristic to improve the performance.
Finally, we conduct an empirical evaluation to assess the viability of our approach.
△ Less
Submitted 12 June, 2017;
originally announced June 2017.
-
Model Checker Execution Reports
Authors:
Rodrigo Castaño,
Victor Braberman,
Diego Garbervetsky,
Sebastian Uchitel
Abstract:
Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access…
▽ More
Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access information about incomplete checks. We characterize the information that model checkers themselves can provide, in terms of analyzed traces, i.e. sequences of statements, and safe cones, and present the notion of execution reports, which we also formalize. We instantiate these concepts for a family of techniques based on Abstract Reachability Trees and implement the approach using the software model checker CPAchecker. We evaluate our approach empirically and provide examples to illustrate the execution reports produced and the information that can be extracted.
△ Less
Submitted 17 August, 2017; v1 submitted 22 July, 2016;
originally announced July 2016.
-
On Verifying Resource Contracts using Code Contracts
Authors:
Rodrigo Castaño,
Juan Pablo Galeotti,
Diego Garbervetsky,
Jonathan Tapicer,
Edgardo Zoppi
Abstract:
In this paper we present an approach to check resource consumption contracts using an off-the-shelf static analyzer.
We propose a set of annotations to support resource usage specifications, in particular, dynamic memory consumption constraints. Since dynamic memory may be recycled by a memory manager, the consumption of this resource is not monotone. The specification language can express both…
▽ More
In this paper we present an approach to check resource consumption contracts using an off-the-shelf static analyzer.
We propose a set of annotations to support resource usage specifications, in particular, dynamic memory consumption constraints. Since dynamic memory may be recycled by a memory manager, the consumption of this resource is not monotone. The specification language can express both memory consumption and lifetime properties in a modular fashion.
We develop a proof-of-concept implementation by extending Code Contracts' specification language. To verify the correctness of these annotations we rely on the Code Contracts static verifier and a points-to analysis. We also briefly discuss possible extensions of our approach to deal with non-linear expressions.
△ Less
Submitted 5 January, 2014;
originally announced January 2014.
