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é de Montpellier)
Charles Dramé-Maigné
(LIRMM, Université de Montpellier)

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.

In Matt Luckcuck and Marie Farrell: Proceedings Fourth International Workshop on Formal Methods for Autonomous Systems (FMAS) and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE) (FMAS2022 ASYDE2022), Berlin, Germany, 26th and 27th of September 2022, Electronic Proceedings in Theoretical Computer Science 371, pp. 120–138.
Published: 27th September 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.371.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org