SkiNet, a petri net generation tool for the verification of skillset-based autonomous systems

B Pelletier, C Lesire, D Doose… - EPTCS 2022-Electronic …, 2022 - hal.science
B Pelletier, C Lesire, D Doose, K Godary-Dejean, C Dramé-Maigné
EPTCS 2022-Electronic Proceedings in Theoretical Computer Science, 2022hal.science
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 …
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.
hal.science
以上显示的是最相近的搜索结果。 查看全部搜索结果