SkiNet, A Petri Net Generation Tool for the Verification of Skillset-based Autonomous Systems

TL;DR

SkiNet is a tool that converts skill-based autonomous system architectures into Petri nets, enabling formal verification of system behaviors and robustness through model-checking techniques.

Contribution

The paper introduces SkiNet, a novel tool that models skill-based architectures as Petri nets for improved verification of autonomous systems.

Findings

Enables formal verification of skill-based systems using Petri nets.

Supports model-checking with LTL and CTL for robustness analysis.

Bridges the gap between system modeling and verification in autonomous robotics.

Abstract

The need for high-level autonomy and robustness of autonomous systems for missions in dynamic and remote environment has pushed developers to come up with new software architectures. A common architecture style is to summarize the capabilities of the robotic system into elementary actions, called skills, on top of which a skill management layer is implemented to structure, test and control the functional layer. However, current available verification tools only provide either mission-specific verification or verification on a model that does not replicate the actual execution of the system, which makes it difficult to ensure its robustness to unexpected events. To that end, a tool, SkiNet, has been developed to transform the skill-based architecture of a system into a Petri net modeling the state-machine behaviors of the skills and the resources they handle. The Petri net allows the use of model-checking, such as Linear Temporal Logic (LTL) or Computational Tree Logic (CTL), for the user to analyze and verify the model of the system.