Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Modelling and Analysis of a Self-Adaptive Robotic System

Juliane Päßler, Maurice H. ter Beek, Ferruccio Damiani, S. Lizeth Tapia Tarifa, Einar Broch Johnsen

TL;DR

The paper tackles uncertainty in autonomous, self-adaptive systems by modeling a two-layer SAS for an autonomous underwater vehicle (AUV) performing pipeline inspection. It advances a feature-aware probabilistic approach using ProFeat, enabling a family-based analysis where the managed subsystem is a probabilistic featured transition system and the managing subsystem is a runtime feature controller that dynamically switches configurations based on environmental and internal states. Through a case study, it demonstrates how to quantify mission duration and energy use via reward properties and assess safety by analyzing unsafe states, across multiple scenarios. The work highlights the feasibility and advantages of analyzing SASs as families, with implications for scalable design and adaptive control strategies in marine robotics, while outlining future work on scaling, optimization of the managing subsystem, and real-world data integration.

Abstract

Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.

Formal Modelling and Analysis of a Self-Adaptive Robotic System

TL;DR

The paper tackles uncertainty in autonomous, self-adaptive systems by modeling a two-layer SAS for an autonomous underwater vehicle (AUV) performing pipeline inspection. It advances a feature-aware probabilistic approach using ProFeat, enabling a family-based analysis where the managed subsystem is a probabilistic featured transition system and the managing subsystem is a runtime feature controller that dynamically switches configurations based on environmental and internal states. Through a case study, it demonstrates how to quantify mission duration and energy use via reward properties and assess safety by analyzing unsafe states, across multiple scenarios. The work highlights the feasibility and advantages of analyzing SASs as families, with implications for scalable design and adaptive control strategies in marine robotics, while outlining future work on scaling, optimization of the managing subsystem, and real-world data integration.

Abstract

Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.
Paper Structure (23 sections, 6 figures, 2 tables)

This paper contains 23 sections, 6 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Outline.
  3. Case Study: Pipeline Inspection by AUV
  4. Two-layered View of the AUV.
  5. Modelling the AUV Case Study with ProFeat
  6. The Feature Model
  7. The Root Feature.
  8. Ordinary Features.
  9. The Managed Subsystem
  10. The Behavioural Model of the Managed Subsystem.
  11. The ProFeat Implementation of the Managed Subsystem.
  12. The Environment
  13. The Behavioural Model of the Environment.
  14. The Implementation of the Environment in ProFeat.
  15. The Managing Subsystem
  16. ...and 8 more sections

Figures (6)

  • Figure 1: Two-level SAS architecture
  • Figure 2: Feature model of the case study
  • Figure 3: The managed subsystem of the AUV
  • Figure 4: The behaviour of the environment
  • Figure 5: The managing subsystem of the AUV
  • ...and 1 more figures