Towards Safety Assessment of Robot Behaviors in SMACH

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Due to the critical consequences of possible failures, robot systems must be formally verified to guarantee that their behaviors are correct and safe. There is, however, a gap in terms of building safe behaviors between the formal methods and robotic communities as the latter focuses on informal design and its implementation in a manner which is accessible to robotics engineers. In this paper, we present an approach to bridge that gap which enables a tight coupling of informal robot behaviors defined in SMACH, Python state machine API, with formal models through a process of translation. A set of mapping rules, which facilitates transformation is provided and the result is utilized for formal verification of safety properties. We also discuss the current limitations of such work along with recommendations on how these might be addressed.

Original languageEnglish
Title of host publicationProceedings - 2023 30th Asia-Pacific Software Engineering Conference, APSEC 2023
Number of pages5
PublisherIEEE Computer Society
Publication date2023
Pages617-621
ISBN (Electronic)9798350344172
DOIs
Publication statusPublished - 2023
Event30th Asia-Pacific Software Engineering Conference, APSEC 2023 - Seoul, Korea, Republic of
Duration: 4. Dec 20237. Dec 2023

Conference

Conference30th Asia-Pacific Software Engineering Conference, APSEC 2023
Country/TerritoryKorea, Republic of
CitySeoul
Period04/12/202307/12/2023
SeriesProceedings of the Asia-Pacific Software Engineering Conference, APSEC
ISSN1530-1362

Keywords

  • Model Checking
  • Robot Behaviors
  • Safety
  • SMACH
  • Timed Automata

Fingerprint

Dive into the research topics of 'Towards Safety Assessment of Robot Behaviors in SMACH'. Together they form a unique fingerprint.

Cite this