Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2401.04875 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910293015134208 |
|---|---|
| author | Kobayashi, Tsutomu Bondu, Martin Ishikawa, Fuyuki |
| author_facet | Kobayashi, Tsutomu Bondu, Martin Ishikawa, Fuyuki |
| contents | Ensuring the safety of autonomous vehicles (AVs) is the key requisite for their acceptance in society. This complexity is the core challenge in formally proving their safety conditions with AI-based black-box controllers and surrounding objects under various traffic scenarios. This paper describes our strategy and experience in modelling, deriving, and proving the safety conditions of AVs with the Event-B refinement mechanism to reduce complexity. Our case study targets the state-of-the-art model of goal-aware responsibility-sensitive safety to argue over interactions with surrounding vehicles. We also employ the Simplex architecture to involve advanced black-box AI controllers. Our experience has demonstrated that the refinement mechanism can be effectively used to gradually develop the complex system over scenario variations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_04875 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement Kobayashi, Tsutomu Bondu, Martin Ishikawa, Fuyuki Software Engineering Ensuring the safety of autonomous vehicles (AVs) is the key requisite for their acceptance in society. This complexity is the core challenge in formally proving their safety conditions with AI-based black-box controllers and surrounding objects under various traffic scenarios. This paper describes our strategy and experience in modelling, deriving, and proving the safety conditions of AVs with the Event-B refinement mechanism to reduce complexity. Our case study targets the state-of-the-art model of goal-aware responsibility-sensitive safety to argue over interactions with surrounding vehicles. We also employ the Simplex architecture to involve advanced black-box AI controllers. Our experience has demonstrated that the refinement mechanism can be effectively used to gradually develop the complex system over scenario variations. |
| title | Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2401.04875 |