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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.371.9 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |