Published January 1, 2019 | Version v1
Publication Open

Hierarchical Coloured Petri-Net Based Multi-Agent System for Flood Monitoring, Prediction, and Rescue (FMPR)

  • 1. Islamia University of Bahawalpur
  • 2. Virtual University of Pakistan
  • 3. Forman Christian College
  • 4. Khwaja Fareed University of Engineering and Information Technology
  • 5. Bahauddin Zakariya University

Description

In Punjab Pakistan, a river flood event is the most important natural disasters that every year causes high human casualties as well as heavy economic losses. A safety-critical system should be correct, reliable, complete, consistent, and unambiguous for accurate and precise flood monitoring, prediction, as well as emergency and rescue services during or after a flood event. System correctness must be ensured in every phase of the development of a safety-critical Flood Monitoring, Prediction, and Rescue (FMPR) system. Correctness is a functional property related to the behavior of the system having sub-properties of safety and liveness. These sub-properties must also be correct, complete, consistent, and unambiguous. Rigorous mathematical based software engineering methods like formal methods are suitable for the specification, design, modeling, verification, and validation of an FMPR safety-critical system. The proposed safety-critical system for FMPR is distributed as it is based on multi-agents. This system is specified, analyzed and designed by using Gaia multi-agent methodology, which is based on organizational abstractions. Gaia role model-based agent roles are specified, regular expression based liveness properties are specified, and first-order predicate calculus based safety properties are specified. Thus, safety and liveness properties are formally specified. After the detailed design phase, the system is formally modeled and verified by Hierarchical Coloured-Petri Nets (CP-Nets). As a result, a novel formal system for the specification, analysis, design, modeling, and verification of the FMPR system is proposed. This safety-critical system is distributed based on multi-agents.

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

Translated Description (Arabic)

في البنجاب باكستان، يعد حدث الفيضان النهري أهم الكوارث الطبيعية التي تتسبب كل عام في خسائر بشرية كبيرة بالإضافة إلى خسائر اقتصادية فادحة. يجب أن يكون النظام الحرج للسلامة صحيحًا وموثوقًا وكاملاً ومتسقًا ولا لبس فيه لمراقبة الفيضانات والتنبؤ بها بدقة ودقة، بالإضافة إلى خدمات الطوارئ والإنقاذ أثناء أو بعد حدوث الفيضان. يجب ضمان صحة النظام في كل مرحلة من مراحل تطوير نظام مراقبة الفيضانات الحرجة والتنبؤ بها وإنقاذها (FMPR). التصحيح هو خاصية وظيفية تتعلق بسلوك النظام الذي يتمتع بخصائص فرعية للسلامة والحيوية. يجب أن تكون هذه الخصائص الفرعية صحيحة وكاملة ومتسقة ولا لبس فيها. تعد طرق هندسة البرمجيات الرياضية الصارمة مثل الطرق الرسمية مناسبة لمواصفات وتصميم ونمذجة والتحقق والتحقق من صحة نظام السلامة الحرجة FMPR. يتم توزيع نظام السلامة الحرجة المقترح لـ FMPR لأنه يعتمد على عوامل متعددة. يتم تحديد هذا النظام وتحليله وتصميمه باستخدام منهجية Gaia متعددة الوكلاء، والتي تستند إلى التجريدات التنظيمية. يتم تحديد أدوار الوكيل القائم على نموذج GAIA، ويتم تحديد خصائص الحياة القائمة على التعبير العادي، ويتم تحديد خصائص السلامة القائمة على حساب التفاضل والتكامل الأصلية من الدرجة الأولى. وبالتالي، يتم تحديد خصائص السلامة والحياة رسميًا. بعد مرحلة التصميم التفصيلي، تتم نمذجة النظام رسميًا والتحقق منه بواسطة شبكات البتري الملونة الهرمية (CP - Nets). ونتيجة لذلك، يُقترح نظام رسمي جديد لمواصفات وتحليل وتصميم ونمذجة والتحقق من نظام FMPR. يتم توزيع هذا النظام الحيوي للسلامة على أساس عوامل متعددة.

Translated Description (French)

Au Pendjab pakistanais, les inondations fluviales sont les catastrophes naturelles les plus importantes qui causent chaque année de nombreuses victimes humaines ainsi que de lourdes pertes économiques. Un système critique pour la sécurité doit être correct, fiable, complet, cohérent et sans ambiguïté pour une surveillance précise et précise des inondations, des prévisions, ainsi que des services d'urgence et de secours pendant ou après une inondation. L'exactitude du système doit être assurée à chaque phase du développement d'un système de surveillance, de prévision et de sauvetage des inondations (FMPR) critique pour la sécurité. La correction est une propriété fonctionnelle liée au comportement du système ayant des sous-propriétés de sécurité et de vivacité. Ces sous-propriétés doivent également être correctes, complètes, cohérentes et sans ambiguïté. Des méthodes rigoureuses d'ingénierie logicielle basées sur les mathématiques, telles que les méthodes formelles, conviennent à la spécification, à la conception, à la modélisation, à la vérification et à la validation d'un système critique pour la sécurité FMPR. Le système critique pour la sécurité proposé pour FMPR est distribué car il est basé sur des multi-agents. Ce système est spécifié, analysé et conçu en utilisant la méthodologie multi-agents Gaia, qui est basée sur des abstractions organisationnelles. Les rôles d'agent basés sur un modèle de rôle Gaia sont spécifiés, les propriétés de vivacité basées sur une expression régulière sont spécifiées et les propriétés de sécurité basées sur le calcul de prédicat de premier ordre sont spécifiées. Ainsi, les propriétés de sécurité et de vivacité sont formellement spécifiées. Après la phase de conception détaillée, le système est formellement modélisé et vérifié par des réseaux de Petri colorés hiérarchiques (CP-Nets). En conséquence, un nouveau système formel pour la spécification, l'analyse, la conception, la modélisation et la vérification du système FMPR est proposé. Ce système critique pour la sécurité est distribué sur la base de multi-agents.

Translated Description (Spanish)

En el Punjab, Pakistán, las inundaciones fluviales son los desastres naturales más importantes que cada año causan un alto número de víctimas humanas, así como grandes pérdidas económicas. Un sistema crítico para la seguridad debe ser correcto, confiable, completo, consistente e inequívoco para un monitoreo y predicción de inundaciones precisos y precisos, así como para los servicios de emergencia y rescate durante o después de una inundación. Se debe garantizar la corrección del sistema en cada fase del desarrollo de un sistema de monitoreo, predicción y rescate de inundaciones (FMPR) crítico para la seguridad. La corrección es una propiedad funcional relacionada con el comportamiento del sistema que tiene subpropiedades de seguridad y vitalidad. Estas subpropiedades también deben ser correctas, completas, consistentes e inequívocas. Los métodos rigurosos de ingeniería de software basados en matemáticas, como los métodos formales, son adecuados para la especificación, el diseño, el modelado, la verificación y la validación de un sistema crítico para la seguridad de FMPR. El sistema crítico de seguridad propuesto para FMPR se distribuye ya que se basa en múltiples agentes. Este sistema se especifica, analiza y diseña utilizando la metodología multiagente de Gaia, que se basa en abstracciones organizativas. Se especifican los roles de agente basados en el modelo de roles de Gaia, se especifican las propiedades de vida basadas en la expresión regular y se especifican las propiedades de seguridad basadas en el cálculo de predicados de primer orden. Por lo tanto, se especifican formalmente las propiedades de seguridad y vitalidad. Después de la fase de diseño detallado, el sistema es modelado y verificado formalmente por Redes de Petri de Colores Jerárquicos (CP-Nets). Como resultado, se propone un nuevo sistema formal para la especificación, análisis, diseño, modelado y verificación del sistema FMPR. Este sistema crítico para la seguridad se distribuye en base a múltiples agentes.

Files

08926354.pdf.pdf

Files (245 Bytes)

⚠️ 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:a7b33edf7831cb3c40ebec2412ebb0fd
245 Bytes
Preview Download

Additional details

Additional titles

Translated title (Arabic)
نظام متعدد الوكلاء قائم على شبكة بتري الملونة الهرمية لرصد الفيضانات والتنبؤ بها وإنقاذها (FMPR)
Translated title (French)
Système multiagent coloré hiérarchique basé sur Petri-Net pour la surveillance, la prévision et le sauvetage des inondations (FMPR)
Translated title (Spanish)
Sistema multiagente jerárquico de color basado en Petri-Net para el monitoreo, predicción y rescate de inundaciones (FMPR)

Identifiers

Other
https://openalex.org/W2998605948
DOI
10.1109/access.2019.2958258

GreSIS Basics Section

Is Global South Knowledge
Yes
Country
Pakistan

References

  • https://openalex.org/W120333500
  • https://openalex.org/W1543548877
  • https://openalex.org/W1595871524
  • https://openalex.org/W1612453857
  • https://openalex.org/W1751549213
  • https://openalex.org/W1934074768
  • https://openalex.org/W1965215820
  • https://openalex.org/W1984957636
  • https://openalex.org/W1988808695
  • https://openalex.org/W2009983102
  • https://openalex.org/W2023104459
  • https://openalex.org/W2033546932
  • https://openalex.org/W2060815669
  • https://openalex.org/W2068770392
  • https://openalex.org/W2100163225
  • https://openalex.org/W2105656578
  • https://openalex.org/W2111877087
  • https://openalex.org/W2117189826
  • https://openalex.org/W2119610731
  • https://openalex.org/W2129899354
  • https://openalex.org/W2142340571
  • https://openalex.org/W2146220225
  • https://openalex.org/W2150189917
  • https://openalex.org/W2164290361
  • https://openalex.org/W2165159570
  • https://openalex.org/W2497585850
  • https://openalex.org/W2602799623
  • https://openalex.org/W2735669400
  • https://openalex.org/W2803481836
  • https://openalex.org/W2912640545
  • https://openalex.org/W3141876048
  • https://openalex.org/W4238198829
  • https://openalex.org/W4245157807
  • https://openalex.org/W4249484115