Heterogeneous Verification of an Autonomous Curiosity Rover

Book chapter


Cardoso, R. C., Farrell, M., Luckcuck, M., Ferrando, A. and Fisher, M. 2020. Heterogeneous Verification of an Autonomous Curiosity Rover. in: Lee, R., Jha, S., Mavridou, A. and Giannakopoulou, D. (ed.) NASA Formal Methods Switzerland Springer. pp. 353–360
AuthorsCardoso, R. C., Farrell, M., Luckcuck, M., Ferrando, A. and Fisher, M.
EditorsLee, R., Jha, S., Mavridou, A. and Giannakopoulou, D.
Abstract

The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4–24 min for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance.

KeywordsNASA; Curiosity rover; planetary exploration mission; heterogeneous verification techniques
Page range353–360
Year2020
Book titleNASA Formal Methods
PublisherSpringer
Place of publicationSwitzerland
SeriesLecture Notes in Computer Science
ISBN9783030557539
9783030557546
ISSN0302-9743
1611-3349
Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-030-55754-6_20
Web address (URL)https://livrepository.liverpool.ac.uk/3100545/
http://dx.doi.org/10.1007/978-3-030-55754-6_20
Output statusPublished
Publication dates10 Aug 2020
Publication process dates
Deposited31 Jan 2023
Permalink -

https://repository.derby.ac.uk/item/9w930/heterogeneous-verification-of-an-autonomous-curiosity-rover

  • 14
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as

Related outputs

CSP2Turtle: Verified Turtle Robot Plans
Dara MacConville, Marie Farrell, Luckcuck, M. and Rosemary Monahan 2023. CSP2Turtle: Verified Turtle Robot Plans. Robotics. 12 (62), pp. 1-22. https://doi.org/10.3390/robotics12020062
An Abstract Architecture for Explainable Autonomy in Hazardous Environments
Matt Luckcuck, Hazel M Taylor and Marie Farrell 2022. An Abstract Architecture for Explainable Autonomy in Hazardous Environments. 2022 IEEE 30th International Requirements Engineering Conference Workshops (REW). IEEE Xplore. https://doi.org/10.1109/rew56159.2022.00027
Modelling the Turtle Python library in CSP
MacConville, D., Farrell, M., Matt Luckcuck and Monahan, R. 2022. Modelling the Turtle Python library in CSP. Second Workshop on Agents and Robots for reliable Engineered Autonomy. Open Publishing Association, Australia. https://doi.org/10.4204/eptcs.362.4
Bridging the gap between single- and multi-model predictive runtime verification
Angelo Ferrando, Rafael C. Cardoso, Marie Farrell, Matt Luckcuck, Fabio Papacchini, Michael Fisher and Viviana Mascardi 2022. Bridging the gap between single- and multi-model predictive runtime verification. Formal Methods in System Design. 59, p. 44–76. https://doi.org/10.1007/s10703-022-00395-7
Formal Verification of a Map Merging Protocol in the Multi-agent Programming Contest
Luckcuck, M. and Cardoso, R. C. 2022. Formal Verification of a Map Merging Protocol in the Multi-agent Programming Contest. in: Alechina, N., Baldoni, M. and Logan, B. (ed.) Engineering Multi-Agent Systems Switzerland Springer. pp. 198–217
Evolution of the IEEE P7009 Standard: Towards Fail-Safe Design of Autonomous Systems
Farrell, M., Luckcuck, M., Pullum, L., Fisher, M., Hessami, A., Danit, G., Murahwi, Z. and Wallace, K. 2022. Evolution of the IEEE P7009 Standard: Towards Fail-Safe Design of Autonomous Systems. 2021 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). IEEE Xplore. https://doi.org/10.1109/issrew53611.2021.00109
Towards Refactoring FRETish Requirements
Farrell, M., Luckcuck, M., Sheridan, O. and Monahan, R. 2022. Towards Refactoring FRETish Requirements. in: Deshmukh, J. V., Havelund, K. and Perez, I. (ed.) NASA Formal Methods Switzerland Springer. pp. 272–279
FRETting About Requirements: Formalised Requirements for an Aircraft Engine Controller
Farrell, M., Luckcuck, M., Sheridan, O. and Monahan, R. 2022. FRETting About Requirements: Formalised Requirements for an Aircraft Engine Controller. in: Gervasi, V. and Vogelsang, A. (ed.) Requirements Engineering: Foundation for Software Quality Switzerland Springer. pp. 96-111
Using formal methods for autonomous systems: Five recipes for formal verification
Luckcuck, M. Using formal methods for autonomous systems: Five recipes for formal verification. Journal of Risk and Reliability. pp. 1-19. https://doi.org/10.1177/1748006x211034970
An Overview of Verification and Validation Challenges for Inspection Robots
Fisher, M., Cardoso, R. C., Collins, E. C., Dadswell, C., Denis, L. A., Dixon, C., Farrell, M., Ferrando, A., Huang, X., Jump, M., Kourtis, G., Lisista, A., Luckcuck, M., Luo, S., Page, V., Papacchini, F. and Webster, M. 2021. An Overview of Verification and Validation Challenges for Inspection Robots. Robotics. 10 (2), pp. 1-29. https://doi.org/10.3390/robotics10020067
MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest
Cardoso, R. C., Ferrando, A., Papacchini, F., Luckcuck, M., Linker, S. and Payne, T. R. 2021. MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest. in: Ahlbrecht, T., Dix, J., Fiekas, N. and Krausburg, T. (ed.) The Multi-Agent Programming Contest 2021 One-and-a-Half Decades of Exploring Multi-Agent Systems Switzerland Springer. pp. 82–107
Towards Compositional Verification for Modular Robotic Systems
Luckcuck, M., Cardoso, R., Dennis, L., Farrell, M. and Fisher, M. 2020. Towards Compositional Verification for Modular Robotic Systems. Second International Workshop on Formal Methods for Autonomous Systems. . https://doi.org/10.4204/eptcs.329.2
Formal specification and verification of autonomous robotic systems: A survey
Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C. and Fisher, M. 2019. Formal specification and verification of autonomous robotic systems: A survey. ACM Computing Surveys. 52 (5), pp. 1-41. https://doi.org/10.1145/3342355
A Summary of Formal Specification and Verification of Autonomous Robotic Systems
Luckcuck, M., Farrell, M., Denis, L. A., Dixon, C. and Fisher, M. 2019. A Summary of Formal Specification and Verification of Autonomous Robotic Systems. in: Ahrendt, W. and Tarifa, S. L. T. (ed.) Integrated Formal Methods Switzerland Springer. pp. 538–541
Robotics and Integrated Formal Methods: Necessity Meets Opportunity
Luckcuck, M., Farrell, M. and Fisher, M. 2018. Robotics and Integrated Formal Methods: Necessity Meets Opportunity. in: Furia, C. A. and Winter, K. (ed.) Integrated Formal Methods Switzerland Springer. pp. 161–171
Verifiable Self-Certifying Autonomous Systems
Fisher, M., Collins, E., Dennis, L., Luckcuck, M., Webster, M., Jump, M., Page, V., Patchett, C., Dinmohammadi, F., Flynn, D., Robu, V. and Zhao, X. 2018. Verifiable Self-Certifying Autonomous Systems. 29th IEEE International Symposium on Software Reliability Engineering Workshops, ISSREW 2018. IEEE Xplore. https://doi.org/10.1109/issrew.2018.00028
A Formal Model of the Safety-Critical Java Level 2 Paradigm
Luckcuck, M., Cavalcanti, A. and Wellings, A. 2016. A Formal Model of the Safety-Critical Java Level 2 Paradigm. in: Ábrahám, E. and Huisman, M. (ed.) Integrated Formal Methods Switzerland Springer. pp. 226–241
Safety-Critical Java: level 2 in practice
Luckcuck, M., Wellings, A. and Cavalcanti, A. 2016. Safety-Critical Java: level 2 in practice. Concurrency Computation. https://doi.org/10.1002/cpe.3951
A Formal Model for the SCJ Level 2 Paradigm
Luckcuck, M. 2015. A Formal Model for the SCJ Level 2 Paradigm. Doctoral Symposium of Formal Methods 2015. University of Oslo.