Published May 6, 2023
| Version v1
Publication
Open
Formal verification of reconfigurable systems
Creators
- 1. California State University, Long Beach
- 2. Shaheed Zulfiqar Ali Bhutto Institute of Science and Technology
- 3. Bahria University
- 4. University of North Carolina at Charlotte
- 5. COMSATS University Islamabad
Description
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.
Translated Descriptions
⚠️
This is an automatic machine translation with an accuracy of 90-95%
Translated Description (Arabic)
الأتمتة هي واحدة من أهم الاتجاهات التكنولوجية في مجال التعدين. تمكن الأتمتة شركات التعدين من العمل على مدار الساعة وزيادة الإنتاجية. توفر الروبوتات درجة جديدة من الأمان للمناجم، من التدريبات الميكانيكية إلى شاحنات الخام ذاتية القيادة. ومع ذلك، فإن تصميم نظام روبوتي يمثل تحديًا لأنهم يعملون في مساحات صغيرة، أو يحفرون المناجم عندما تكون هناك صخور صلبة، أو يمكن أن يلحقوا الضرر بأنفسهم عن طريق التمدد المفرط أو التراجع. تعد سلامة هذه الروبوتات ضرورية أيضًا لضمان عملها بشكل صحيح. صممت هذه الورقة رسميًا ذراع تعدين روبوتية يمكن أن تلحق الضرر بنفسها إذا فشل المستشعر. يوضح هذا التقرير كيف يمكن منع الضرر الناجم عن فشل المستشعر من خلال نمذجة النظام رسميًا والتأكد من أنه لن يتلف نفسه. علاوة على ذلك، فإن ذراعنا الروبوتية قابلة لإعادة التشكيل وقادرة على التعامل مع المواقف الخطرة. قمنا رسميًا بنمذجة نظامنا باستخدام أداة فحص النموذج UPPAAL وتحققنا من النظام في المواقف الخطرة المختلفة. يتم التحقق من النظام من حيث السلامة والحيوية والإنصاف والقيود الخالية من الرؤية. تظهر النتائج أن المنهجية مناسبة لنمذجة ومحاكاة والتحقق من الأنظمة القابلة لإعادة التكوين.Translated Description (French)
L'automatisation est l'une des principales tendances technologiques dans le secteur minier. L'automatisation permet aux sociétés minières de travailler 24 heures sur 24 et de maximiser la productivité. La robotique apporte un nouveau degré de sécurité aux mines, des foreuses mécaniques aux camions de minerai autonomes. Cependant, la conception d'un système robotique est difficile car ils travaillent dans de petits espaces, forent les mines lorsqu'il y a des roches dures ou peuvent s'endommager en se déployant ou en se rétractant. La sécurité de ces robots est également essentielle pour s'assurer qu'ils fonctionnent correctement. Ce document a formellement modélisé un bras d'extraction robotisé qui pourrait s'endommager en cas de défaillance d'un capteur. Ce rapport montre comment les dommages causés par une défaillance du capteur peuvent être évités en modélisant formellement le système et en veillant à ce qu'il ne s'endommage pas lui-même. De plus, notre bras robotique est reconfigurable et capable de faire face à des situations dangereuses. Nous avons formellement modélisé notre système à l'aide d'un outil de vérification de modèle UPPAAL et vérifié le système dans diverses situations dangereuses. Le système est vérifié pour la sécurité, la vivacité, l'équité et les contraintes sans impasse. Les résultats montrent que la méthodologie est adaptée pour modéliser, simuler et vérifier des systèmes reconfigurables.Translated Description (Spanish)
La automatización es una de las principales tendencias tecnológicas en la minería. La automatización permite a las empresas mineras trabajar día y noche y maximizar la productividad. La robótica aporta un nuevo grado de seguridad a las minas, desde perforadoras mecánicas hasta camiones de mineral autónomos. Sin embargo, diseñar un sistema robótico es un desafío porque trabajan en espacios pequeños, perforan las minas cuando hay rocas duras o pueden dañarse al extenderse o retraerse demasiado. La seguridad de estos robots también es esencial para garantizar que funcionen correctamente. Este documento modeló formalmente un brazo robótico de minería que podría dañarse a sí mismo si falla un sensor. Este informe demuestra cómo se puede prevenir el daño causado por la falla del sensor modelando formalmente el sistema y asegurándose de que no se dañe a sí mismo. Además, nuestro brazo robótico es reconfigurable y capaz de hacer frente a situaciones peligrosas. Modelamos formalmente nuestro sistema utilizando una herramienta de verificación de modelos UPPAAL y verificamos el sistema en diversas situaciones peligrosas. El sistema se verifica en cuanto a las restricciones de seguridad, vitalidad, equidad y falta de bloqueo. Los resultados muestran que la metodología es adecuada para modelar, simular y verificar sistemas reconfigurables.Files
latest.pdf.pdf
Files
(275 Bytes)
| Name | Size | Download all |
|---|---|---|
|
md5:4ffeadb3e92616e21b5bd26459495e18
|
275 Bytes | Preview Download |
Additional details
Additional titles
- Translated title (Arabic)
- التحقق الرسمي من الأنظمة القابلة لإعادة التكوين
- Translated title (French)
- Vérification formelle des systèmes reconfigurables
- Translated title (Spanish)
- Verificación formal de sistemas reconfigurables
Identifiers
- Other
- https://openalex.org/W4372352988
- DOI
- 10.1007/s00500-023-08272-z
References
- https://openalex.org/W1524364219
- https://openalex.org/W1993466996
- https://openalex.org/W2073544622
- https://openalex.org/W2095178855
- https://openalex.org/W2103631506
- https://openalex.org/W2106417311
- https://openalex.org/W2125100621
- https://openalex.org/W2158849671
- https://openalex.org/W2160883697
- https://openalex.org/W2492982004
- https://openalex.org/W2518005972
- https://openalex.org/W2783159776
- https://openalex.org/W2786169045
- https://openalex.org/W2807765873
- https://openalex.org/W2811472820
- https://openalex.org/W2914206182
- https://openalex.org/W3087808993
- https://openalex.org/W3111902597
- https://openalex.org/W3138754412
- https://openalex.org/W3203094162
- https://openalex.org/W4242741415
- https://openalex.org/W4283517747