Formal Modelling and Analysis of a Self-Adaptive Robotic System
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916090914799616 |
|---|---|
| author | Päßler, Juliane ter Beek, Maurice H. Damiani, Ferruccio Tarifa, S. Lizeth Tapia Johnsen, Einar Broch |
| author_facet | Päßler, Juliane ter Beek, Maurice H. Damiani, Ferruccio Tarifa, S. Lizeth Tapia Johnsen, Einar Broch |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2308_14663 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Formal Modelling and Analysis of a Self-Adaptive Robotic System Päßler, Juliane ter Beek, Maurice H. Damiani, Ferruccio Tarifa, S. Lizeth Tapia Johnsen, Einar Broch Logic in Computer Science Robotics Software Engineering 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. |
| title | Formal Modelling and Analysis of a Self-Adaptive Robotic System |
| topic | Logic in Computer Science Robotics Software Engineering |
| url | https://arxiv.org/abs/2308.14663 |