SkiNet：スキルベース自律システム検証のためのペトリネット生成ツール
SkiNet, A Petri Net Generation Tool for the Verification of Skillset-based Autonomous Systems
スキルベースのロボットアーキテクチャをペトリネットに変換し、モデル検査による検証を可能にするツールSkiNetを開発した。
著者: Baptiste Pelletier, Charles Lesire, David Doose, Karen Godary-Dejean, Charles Dramé-Maigné
分類: cs.FL, cs.RO
原文アブストラクト
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.
