论文标题
Skinet，一种用于验证基于技能的自主系统的Petri Net生成工具
SkiNet, A Petri Net Generation Tool for the Verification of Skillset-based Autonomous Systems
论文作者
论文摘要
在动态和远程环境中，对自主系统的高级自主性和鲁棒性的需求促使开发人员提出了新的软件体系结构。一种常见的体系结构样式是将机器人系统的功能总结为基本动作（称为技能），其顶部是在该动作中实施技能管理层以结构，测试和控制功能层。但是，当前可用的验证工具仅在不复制系统实际执行的模型上提供特定于任务的验证或验证，这使得难以确保其对意外事件的鲁棒性。为此，已经开发了一种工具Skinet，以将系统的基于技能的架构转换为Petri网络，以建模技能和资源的状态机器行为。 Petri NET允许使用模型检查，例如线性时间逻辑（LTL）或计算树逻辑（CTL），以供用户分析和验证系统的模型。
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.
