Modeling and formal verification of IMPP
المؤلفون المشاركون
Khan, Sohel
Abd al-Sattar, Abd al-Wahid
المصدر
The International Arab Journal of Information Technology
العدد
المجلد 2، العدد 3 (31 يوليو/تموز 2005)، ص ص. 192-198، 7ص.
الناشر
تاريخ النشر
2005-07-31
دولة النشر
الأردن
عدد الصفحات
7
التخصصات الرئيسية
تكنولوجيا المعلومات وعلم الحاسوب
الموضوعات
الملخص EN
This paper describes the modeling and formal verification of the application layer protocol, Instant Messaging and Presence Protocol (IMPP).
Spin is a model checker for the verification of asynchronous, distributed and concurrent finite state systems.
It accepts the system specification in a high level language called PROcess MEta LAnguage (PROMELA) and verification claims in temporal logic.
We have selected Instant Messaging and Presence Protocol (IMPP) for modeling, simulation and verification as it is characterized by concurrency and distributed computing, which makes it a good candidate to explore the potential of model checking and verification.
Further, the important properties of the protocol are verified using Linear Temporal Logic (LTL).
One of our aims was also to get an insight into the scope and utility of formal methods based on state space exploration in testing larger and complex software systems which has been achieved to some extent.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Khan, Sohel& Abd al-Sattar, Abd al-Wahid. 2005. Modeling and formal verification of IMPP. The International Arab Journal of Information Technology،Vol. 2, no. 3, pp.192-198.
https://search.emarefa.net/detail/BIM-12169
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Khan, Sohel& Abd al-Sattar, Abd al-Wahid. Modeling and formal verification of IMPP. The International Arab Journal of Information Technology Vol. 2, no. 3 (Jul. 2005), pp.192-198.
https://search.emarefa.net/detail/BIM-12169
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Khan, Sohel& Abd al-Sattar, Abd al-Wahid. Modeling and formal verification of IMPP. The International Arab Journal of Information Technology. 2005. Vol. 2, no. 3, pp.192-198.
https://search.emarefa.net/detail/BIM-12169
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references : p. 197-198
رقم السجل
BIM-12169
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر