Verification for space robotics

摘要

Chapter Contents: 11.1 Formal specification and verification techniques 11.1.1 Formal specification and verification for autonomous robotic systems 11.1.1.1 Methodology 11.1.1.2 Answering RQ1: challenges 11.1.1.3 Answering RQ2: formalisms, tools and approaches 11.1.1.4 Answering RQ3: limitations 11.1.1.5 Application to space robotics 11.2 Theorem proving for space robotics using modal and temporal logics 11.2.1 The multi-modal logic K 11.2.2 Metric temporal logic 11.3 Verifiable space robot architectures 11.3.1 FOL contract specifications 11.3.2 Measuring confidence in verification 11.3.3 Related work 11.4 Case study 1: Simulation and verification of the Mars Curiosity rover 11.4.1 Simulation 11.4.2 Model checking 11.4.3 Runtime verification 11.5 Case study 2: Verification of astronaut—rover teams 11.6 Modelling and verification of multi-objects systems 11.6.1 Motivation 11.6.2 Logics for parameterised systems 11.6.3 Translating broadcast protocols to MFOTL 11.7 Conclusions, recommendations and future trends References