Formal Modeling and Analysis of Robotic Arm

Automation is one of the foremost technological trends in mining. Automation empowers mining companies to work around the clock and maximize productivity. Robotics brings a new degree of security to mines, from mechanical drills to self-driving ore trucks. The safety of these robots is also essential to ensure they should not damage themselves. In this paper, we have formally modeled a robotic mining arm mechatronic system that could damage itself if a sensor were to fail. This report demonstrates how the damage caused by sensor failure can be prevented by formally modeling the system and verifiable properties to test that it would not damage itself during a sensor failure. The models and properties developed showed that the system would fail safely in such a scenario. We use the model-checking tool UPPAAL, and all components are modeled using timed automata. The case study is formally modeled using the model-checking tool UPPAAL and verified for safety, liveness, and deadlock-freeness properties.