Designing and Verifying Communication Protocols Using Model Driven Architecture and Spin Model Checker
ABSTRACT
The need of communication protocols in today’s environment increases as much as the network explores. Many new kinds of protocols, e.g. for information sharing, security, etc., are being developed day-to-day which often leads to rapid, premature developments. Many protocols have not scaled to satisfy important properties like deadlock and livelock freedom, since MDA focuses on the rapid development rather than on the quality of the developed models. In order to fix the above, we introduce a 2-Phase strategy based on the UML state machine and sequence diagram. The state machine is converted into PROMELA code as a protocol model and its properties are derived from the sequence diagram as Linear Temporal Logic (LTL) through automation. The PROMELA code is interpreted through the SPIN model checker, which helps to simulate the behavior of protocol. Later the automated LTL properties are supplemented to the SPIN for the verification of protocol properties. The results are compared with the developed UML model and SPIN simulated model. Our test results impress the designer to verify the expected results with the system design and to identify the errors which are unnoticed during the design phase.
The need of communication protocols in today’s environment increases as much as the network explores. Many new kinds of protocols, e.g. for information sharing, security, etc., are being developed day-to-day which often leads to rapid, premature developments. Many protocols have not scaled to satisfy important properties like deadlock and livelock freedom, since MDA focuses on the rapid development rather than on the quality of the developed models. In order to fix the above, we introduce a 2-Phase strategy based on the UML state machine and sequence diagram. The state machine is converted into PROMELA code as a protocol model and its properties are derived from the sequence diagram as Linear Temporal Logic (LTL) through automation. The PROMELA code is interpreted through the SPIN model checker, which helps to simulate the behavior of protocol. Later the automated LTL properties are supplemented to the SPIN for the verification of protocol properties. The results are compared with the developed UML model and SPIN simulated model. Our test results impress the designer to verify the expected results with the system design and to identify the errors which are unnoticed during the design phase.
Cite this paper
nullP. Kaliappan and H. Koenig, "Designing and Verifying Communication Protocols Using Model Driven Architecture and Spin Model Checker," Journal of Software Engineering and Applications, Vol. 1 No. 1, 2008, pp. 13-19. doi: 10.4236/jsea.2008.11003.
nullP. Kaliappan and H. Koenig, "Designing and Verifying Communication Protocols Using Model Driven Architecture and Spin Model Checker," Journal of Software Engineering and Applications, Vol. 1 No. 1, 2008, pp. 13-19. doi: 10.4236/jsea.2008.11003.
References
[1] C. Werner, “UML profile for communicating systems,” Ph.D thesis, University of Gottingen, Department of Computer Science, 2006. [2] Unified Modeling Language, The official homepage of UML, Object Management Group. [3] Model Driven Architecture: A Technical Perspective, Architecture Board MDA Drafting Team, Document [4] Process Meta Language. [5] G. J. Holzmann, “The model checker SPIN,” IEEE Transactions on Software Engineering, 23 (1997) 5: pp. 279–295, 1997. [6] M. Farid, G. Patrice, and B. Mourad, “Verifying UML diagrams with model checking: A rewriting logic based approach,” Seventh International Conference on Quality Software (QSIC 2007), pp. 356–362, 2007. [7] S. Wuwei, C. Kevinon, and H. James, “A toolset for supporting UML static and dynamic model checking,” 26th Annual International Computer Software and Applications Conference, 2002. [8] B. Prasanta, “Automated translation of UML models of architectures for verification and simulation using SPIN.,” 14th IEEE International Conference on Automated Software Engineering (ASE’99), pp. 102–109, 1999. [9] S. W. Vitus and J. Padget, “Symbolic Model Checking of UML Statechart Diagrams with an Integrated Approach,” 11th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems (ECBS’04), pp. 337–346, 2004. [10] A. Kleppe, J. Warmer, and W. Bast, “MDA Explained—The Model Driven Architecture: Practice and Promise,” Addison-Wesley, 2003. [11] Query, Views, Transformations: A Specification document. http://www.omg.org/technology/documents/modeling spec catalog.htm. [12] eXample Data Transfer (XDT) Protocol. http://www.protocol-engineering.tu-cottbus.de/index_xdt.htm [13] E. M. Clarke, O. Grumberg, and D. Peled, “Model checking,” MIT Press, 1999.
[1] C. Werner, “UML profile for communicating systems,” Ph.D thesis, University of Gottingen, Department of Computer Science, 2006. [2] Unified Modeling Language, The official homepage of UML, Object Management Group. [3] Model Driven Architecture: A Technical Perspective, Architecture Board MDA Drafting Team, Document [4] Process Meta Language. [5] G. J. Holzmann, “The model checker SPIN,” IEEE Transactions on Software Engineering, 23 (1997) 5: pp. 279–295, 1997. [6] M. Farid, G. Patrice, and B. Mourad, “Verifying UML diagrams with model checking: A rewriting logic based approach,” Seventh International Conference on Quality Software (QSIC 2007), pp. 356–362, 2007. [7] S. Wuwei, C. Kevinon, and H. James, “A toolset for supporting UML static and dynamic model checking,” 26th Annual International Computer Software and Applications Conference, 2002. [8] B. Prasanta, “Automated translation of UML models of architectures for verification and simulation using SPIN.,” 14th IEEE International Conference on Automated Software Engineering (ASE’99), pp. 102–109, 1999. [9] S. W. Vitus and J. Padget, “Symbolic Model Checking of UML Statechart Diagrams with an Integrated Approach,” 11th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems (ECBS’04), pp. 337–346, 2004. [10] A. Kleppe, J. Warmer, and W. Bast, “MDA Explained—The Model Driven Architecture: Practice and Promise,” Addison-Wesley, 2003. [11] Query, Views, Transformations: A Specification document. http://www.omg.org/technology/documents/modeling spec catalog.htm. [12] eXample Data Transfer (XDT) Protocol. http://www.protocol-engineering.tu-cottbus.de/index_xdt.htm [13] E. M. Clarke, O. Grumberg, and D. Peled, “Model checking,” MIT Press, 1999.