Despite the rise in applications of formal methods for the design and analysis of robotic systems, their integration into existing frameworks remains a challenge. Part of the problem is due to the important changes in the software architecture of robotic design tools needed to accommodate for formal methods, but another challenge is the inherent difficulty for non-experts to use formal methods. In this work, we present SkiNet, a user-oriented tool which aims to assist in the design of skill-based robotic systems using a formal model based on Petri nets. The main idea for SkiNet is to interpret the user-written specifications and properties, into elements from the formal model, and vice versa. This allows the user to be more independent when diagnosing and validating the specified behavior, without having to directly manipulate the back-end formal tools. An example of the verification process of robotic skills specifications using SkiNet is given to showcase this paradigm.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

SkiNet: A User-Oriented Tool for Petri Net-Based Analysis of Robotic Skills

  • Baptiste Pelletier,
  • Charles Lesire,
  • Karen Godary-Dejean

摘要

Despite the rise in applications of formal methods for the design and analysis of robotic systems, their integration into existing frameworks remains a challenge. Part of the problem is due to the important changes in the software architecture of robotic design tools needed to accommodate for formal methods, but another challenge is the inherent difficulty for non-experts to use formal methods. In this work, we present SkiNet, a user-oriented tool which aims to assist in the design of skill-based robotic systems using a formal model based on Petri nets. The main idea for SkiNet is to interpret the user-written specifications and properties, into elements from the formal model, and vice versa. This allows the user to be more independent when diagnosing and validating the specified behavior, without having to directly manipulate the back-end formal tools. An example of the verification process of robotic skills specifications using SkiNet is given to showcase this paradigm.