Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2411.14373 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909398560931840 |
|---|---|
| author | Raïs, Sylvain Brunel, Julien Doose, David Herbreteau, Frédéric |
| author_facet | Raïs, Sylvain Brunel, Julien Doose, David Herbreteau, Frédéric |
| contents | Robotic systems are widely used to interact with humans or to perform critical tasks. As a result, it is imperative to provide guarantees about their behavior. Due to the modularity and complexity of robotic systems, their design and verification are often divided into several layers. However, some system properties can only be investigated by considering multiple layers simultaneously. We propose a cross-layer verification method to verify the expected properties of concrete robotic systems. Our method verifies one layer using abstractions of other layers. We propose two approaches: refining the models of the abstract layers and refining the property under verification. A combination of these two approaches seems to be the most promising to ensure model genericity and to avoid the state-space explosion problem. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_14373 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Cross--layer Formal Verification of Robotic Systems Raïs, Sylvain Brunel, Julien Doose, David Herbreteau, Frédéric Robotics Robotic systems are widely used to interact with humans or to perform critical tasks. As a result, it is imperative to provide guarantees about their behavior. Due to the modularity and complexity of robotic systems, their design and verification are often divided into several layers. However, some system properties can only be investigated by considering multiple layers simultaneously. We propose a cross-layer verification method to verify the expected properties of concrete robotic systems. Our method verifies one layer using abstractions of other layers. We propose two approaches: refining the models of the abstract layers and refining the property under verification. A combination of these two approaches seems to be the most promising to ensure model genericity and to avoid the state-space explosion problem. |
| title | Cross--layer Formal Verification of Robotic Systems |
| topic | Robotics |
| url | https://arxiv.org/abs/2411.14373 |