Modeling and Formal Verification of IMPP

International Arab Journal of Information Technology (IAJIT)

Maryam Madani¹  Shadpour Mallakpour² 

[1] Department of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Department of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. IranDepartment of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$;Department of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Nanotechnology and Advanced Materials Institute, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Department of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. IranDepartment of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Nanotechnology and Advanced Materials Institute, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Nanotechnology and Advanced Materials Institute, Isfahan University of Technology, Isfahan 84156-83111, I. R. IranDepartment of Chemistry, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$Nanotechnology and Advanced Materials Institute, Isfahan University of Technology, Isfahan 84156-83111, I. R. Iran$$

关键词: Formal methods;    verification of communication protocols;    instant messaging systems;    verification tools;    spin;    LTL;    PROMELA.;   

DOI  :  

学科分类：计算机科学（综合）

来源: Zarqa University

【 摘 要 】

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.Keywords: Formal methods, verification of communication protocols, instant messaging systems, verification tools, spin, LTL, PROMELA.Received March 14, 2004; accepted July 7, 2004Full Text

【 授权许可】

Unknown