Published January 1, 2015 | Version v1
Publication Open

Modeling and Verification of Reconfigurable and Energy-Efficient Manufacturing Systems

Creators

  • 1. Xidian University
  • 2. Saarland University
  • 3. University of Carthage
  • 4. Macau University of Science and Technology
  • 5. King Abdulaziz University

Description

This paper deals with the formal modeling and verification of reconfigurable and energy-efficient manufacturing systems (REMSs) that are considered as reconfigurable discrete event control systems. A REMS not only allows global reconfigurations for switching the system from one configuration to another, but also allows local reconfigurations on components for saving energy when the system is in a particular configuration. In addition, the unreconfigured components of such a system should continue running during any reconfiguration. As a result, during a system reconfiguration, the system may have several possible paths and may fail to meet control requirements if concurrent reconfiguration events and normal events are not controlled. To guarantee the safety and correctness of such complex systems, formal verification is of great importance during a system design stage. This paper extends the formalism reconfigurable timed net condition/event systems (R-TNCESs) in order to model all possible dynamic behavior in such systems. After that, the designed system based on extended R-TNCESs is verified with the help of a software tool SESA for functional, temporal, and energy-efficient properties. This paper is illustrated by an automatic assembly system.

⚠️ This is an automatic machine translation with an accuracy of 90-95%

Translated Description (Arabic)

تتناول هذه الورقة النمذجة الرسمية والتحقق من أنظمة التصنيع القابلة لإعادة التشكيل والموفرة للطاقة (REMSs) التي تعتبر أنظمة تحكم منفصلة في الأحداث قابلة لإعادة التشكيل. لا يسمح نظام REMS فقط بإعادة التهيئة العالمية لتحويل النظام من تكوين إلى آخر، ولكنه يسمح أيضًا بإعادة التهيئة المحلية للمكونات لتوفير الطاقة عندما يكون النظام في تكوين معين. بالإضافة إلى ذلك، يجب أن تستمر المكونات غير المكونة لمثل هذا النظام في العمل أثناء أي إعادة تكوين. نتيجة لذلك، أثناء إعادة تكوين النظام، قد يكون للنظام العديد من المسارات المحتملة وقد يفشل في تلبية متطلبات التحكم إذا لم يتم التحكم في أحداث إعادة التكوين المتزامنة والأحداث العادية. لضمان سلامة وصحة هذه الأنظمة المعقدة، يعد التحقق الرسمي ذا أهمية كبيرة خلال مرحلة تصميم النظام. توسع هذه الورقة أنظمة الحالة/الحدث الصافية الموقوتة القابلة لإعادة التشكيل (R - TNCESs) من أجل نمذجة جميع السلوك الديناميكي المحتمل في مثل هذه الأنظمة. بعد ذلك، يتم التحقق من النظام المصمم بناءً على R - TNCES الموسعة بمساعدة أداة برمجية SESA للخصائص الوظيفية والزمنية والموفرة للطاقة. يتم توضيح هذه الورقة بواسطة نظام تجميع أوتوماتيكي.

Translated Description (French)

Cet article traite de la modélisation formelle et de la vérification des systèmes de fabrication reconfigurables et économes en énergie (rems) qui sont considérés comme des systèmes de contrôle d'événements discrets reconfigurables. Un rems permet non seulement des reconfigurations globales pour commuter le système d'une configuration à une autre, mais permet également des reconfigurations locales sur les composants pour économiser de l'énergie lorsque le système est dans une configuration particulière. En outre, les composants non configurés d'un tel système doivent continuer à fonctionner pendant toute reconfiguration. En conséquence, lors d'une reconfiguration du système, le système peut avoir plusieurs chemins possibles et peut ne pas répondre aux exigences de contrôle si les événements de reconfiguration simultanés et les événements normaux ne sont pas contrôlés. Pour garantir la sécurité et l'exactitude de ces systèmes complexes, la vérification formelle est d'une grande importance lors de la phase de conception du système. Cet article étend le formalisme des systèmes de conditions/événements nets chronométrés reconfigurables (R-TNCES) afin de modéliser tous les comportements dynamiques possibles dans de tels systèmes. Après cela, le système conçu basé sur des R-TNCES étendus est vérifié à l'aide d'un outil logiciel SESA pour des propriétés fonctionnelles, temporelles et économes en énergie. Ce papier est illustré par un système d'assemblage automatique.

Translated Description (Spanish)

Este documento trata sobre el modelado formal y la verificación de sistemas de fabricación reconfigurables y energéticamente eficientes (REMS) que se consideran sistemas de control de eventos discretos reconfigurables. Un REMS no solo permite reconfiguraciones globales para cambiar el sistema de una configuración a otra, sino que también permite reconfiguraciones locales en componentes para ahorrar energía cuando el sistema está en una configuración particular. Además, los componentes no configurados de dicho sistema deben continuar ejecutándose durante cualquier reconfiguración. Como resultado, durante una reconfiguración del sistema, el sistema puede tener varias rutas posibles y puede no cumplir con los requisitos de control si no se controlan los eventos de reconfiguración simultáneos y los eventos normales. Para garantizar la seguridad y la corrección de sistemas tan complejos, la verificación formal es de gran importancia durante una etapa de diseño del sistema. Este documento amplía el formalismo de los sistemas reconfigurables de condiciones/eventos netos cronometrados (R-TNCES) para modelar todo el comportamiento dinámico posible en dichos sistemas. Después de eso, el sistema diseñado basado en R-TNCES extendidos se verifica con la ayuda de una herramienta de software SESA para propiedades funcionales, temporales y de eficiencia energética. Este documento se ilustra mediante un sistema de montaje automático.

Files

813476.pdf.pdf

Files (4.5 kB)

⚠️ Please wait a few minutes before your translated files are ready ⚠️ Note: Some files might be protected thus translations might not work.
Name Size Download all
md5:10365c7234bd3389034648dd551ce057
4.5 kB
Preview Download

Additional details

Additional titles

Translated title (Arabic)
نمذجة أنظمة التصنيع القابلة لإعادة التشكيل والموفرة للطاقة والتحقق منها
Translated title (French)
Modélisation et vérification des systèmes de fabrication reconfigurables et économes en énergie
Translated title (Spanish)
Modelado y verificación de sistemas de fabricación reconfigurables y energéticamente eficientes

Identifiers

Other
https://openalex.org/W1547450940
DOI
10.1155/2015/813476

Is supplement to
https://openalex.org/W2130472321 (Other)
https://openalex.org/W2382672788 (Other)
https://openalex.org/W2387766148 (Other)
https://openalex.org/W2365996311 (Other)
https://openalex.org/W2387500363 (Other)
https://openalex.org/W2544276806 (Other)
https://openalex.org/W2357657342 (Other)
https://openalex.org/W2404647514 (Other)
https://openalex.org/W4242251885 (Other)
https://openalex.org/W1667647204 (Other)

GreSIS Basics Section

Is Global South Knowledge
Yes
Country
Tunisia

References

  • https://openalex.org/W1751549213
  • https://openalex.org/W1915570783
  • https://openalex.org/W1996109622
  • https://openalex.org/W2005217875
  • https://openalex.org/W2010335050
  • https://openalex.org/W2019480338
  • https://openalex.org/W2022250047
  • https://openalex.org/W2035556324
  • https://openalex.org/W2037933704
  • https://openalex.org/W2048456685
  • https://openalex.org/W2049252484
  • https://openalex.org/W2056152068
  • https://openalex.org/W2066555597
  • https://openalex.org/W2076665553
  • https://openalex.org/W2084880958
  • https://openalex.org/W2093676880
  • https://openalex.org/W2100054110
  • https://openalex.org/W2105435021
  • https://openalex.org/W2110169180
  • https://openalex.org/W2113418311
  • https://openalex.org/W2132355828
  • https://openalex.org/W2139473437
  • https://openalex.org/W2140640958
  • https://openalex.org/W2146738006
  • https://openalex.org/W2163338158
  • https://openalex.org/W2163839607
  • https://openalex.org/W2165321755
  • https://openalex.org/W2165594843
  • https://openalex.org/W2310250136