Model Checking Industrial Robot Systems
Model Checking Industrial Robot Systems
复制标题
DOI：
10.1007/978-3-642-22306-8_11
复制
发表时间：
2011-07
期刊：
影响因子：
--
通讯作者：
Markus Weißmann;Stefan Bedenk;C. Buckl;A. Knoll
中科院分区：
文献类型：
--
作者：
Markus Weißmann;Stefan Bedenk;C. Buckl;A. Knoll
现代生产工厂是高度自动化的复杂系统，由多个机器人和其他工作机器组成。导致损坏和生产停止的错误代价极其高昂，必须尽一切努力避免。因此，实践的状态是提前测试控制程序，这意味着大量的努力和高昂的成本。为了增加对控制系统的信心并减少必要的工作，本文建议使用模型检查来验证某些属性。它提供了一个编译器，可以将工业机器人程序转换为 PROMELA 模型。由于机器人编程语言的语句不能直接映射到 PROMELA 语句，因此我们应用编译器优化技术来缩小语义差距。如果发生规范违规，跟踪将映射到原始上下文，以便机器人程序员可以重建问题。作为案例研究，我们应用该工具来验证不存在冲突和死锁。我们能够在拥有 9 个机器人的车身焊接站中检测到一个死锁，纠正程序并验证所得系统的正确性。
Modern production plants are highly automated complex systems consisting of several robots and other working machines. Errors leading to damage and stop of production are extremely expensive and must be avoided by all means. Hence, the state of practice is to test control programs in advance which implies high effort and comes with high costs. To increase the confidence into the control systems and to reduce the necessary effort, this paper proposes to use model checking to verify certain properties. It presents a compiler that can transform industrial robot programs into PROMELA models. Since the statements of the robot programming language can not be mapped directly into PROMELA statements, we apply compiler optimization techniques to close the semantic gap. In case of a specification violation the trace is mapped to the original context so that the robot programmer can reconstruct the problem. As a case study we applied the tool to verify the absence of collisions and deadlocks. We were able to detect one deadlock in a car-body welding station with 9 robots, correct the program and verify the correctness of the resulting system.