Formal verification of reconfigurable systems

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. However, designing a robotic system is challenging because they work in small spaces, drill the mines when there are hard rocks, or can damage themselves by overextending or retracting. The safety of these robots is also essential to ensure they work correctly. This paper formally modeled a robotic mining arm that could damage itself if a sensor fails. This report demonstrates how the damage caused by sensor failure can be prevented by formally modeling the system and ensuring it would not damage itself. Moreover, our robotic arm is reconfigurable and capable of dealing with hazardous situations. We formally modeled our system using a model-checking tool UPPAAL and verified the system in various hazardous situations. The system is verified for safety, liveness, fairness, and deadlock-freeness constraints. The results show that the methodology is suitable for modeling, simulating, and verifying reconfigurable systems.