SkiNet, A Petri Net Generation Tool for the Verification of Skillset-based Autonomous Systems
Baptiste Pelletier (ONERA - The French Aerospace Lab), Charles Lesire, (ONERA - The French Aerospace Lab), David Doose (ONERA - The French Aerospace, Lab), Karen Godary-Dejean (LIRMM, Universit\'e de Montpellier), Charles, Dram\'e-Maign\'e (LIRMM, Universit\'e de Montpellier)

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
