Skip to main content
WorldCist'23 - 11st World Conference on Information Systems and Technologies

Full Program »

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.

Muhammad Abdul Basit Ur Rahim
California State University Long Beach
United States

Seth Bettwieser
Montana Technological University
United States

Andrey Zuev
Montana Technological University Long Beach
United States

Muhammad Ahsan Ur Raheem
Shaheed Zulfikar Ali Bhutto Institute of Science and Technology

Mohammad Farid Atif
University of North Carolina at Charlotte
United States


Powered by OpenConf®
Copyright ©2002-2022 Zakon Group LLC