Implementing Partitioning Detection and Connectivity Restoration in WSAN Using VDM-SL
作者： Hamra Afzaal , Muhammad Imran , Nazir Ahmad Zafar
DOI: 10.1109/FIT.2015.10
关键词: Specification language 、 Distributed computing 、 Correctness 、 Graph (abstract data type) 、 Formal methods 、 Formal verification 、 Toolbox 、 Computer science 、 Software system 、 Formal specification
摘要: Recently the interest in wireless sensor and actor networks has increased tremendously. Although there been significant improvement WSANs, but still many challenges are needed to overcome issues of critical applications. In most published work focus is on performance analysis non-functional properties correctness approach ignored which very important large complex systems. This paper introduces an alternative for formal specification, implementation Partitioning Detection Connectivity Restoration (PCR) algorithm WSANs. We model WSAN as a dynamic graph use VDM-SL describe specification algorithm. Invariants used validate pre post conditions confirm operations. language software systems illustrate detailed level examination. The PCR implemented, verified, validated analyzed through toolbox.
sci-hub.se 参考文章(14)
Nazir Ahmad Zafar, Sher Afzal Khan, Improving moving block railway system using fuzzy multi-agent specification language International Journal of Innovative Computing Information and Control. ,vol. 7, pp. 4517- 4533 ,(2011)
Muhammad Imran, Nazir Ahmad Zafar, Mohammed Abdullah Alnuem, Mehmet Sabih Aksoy, Athanasios V. Vasilakos, Formal verification and validation of a movement control actor relocation algorithm for safety–critical applications Wireless Networks. ,vol. 22, pp. 247- 265 ,(2016) , 10.1007/S11276-015-0962-8
Muhammad Imran, Abas Md. Said, Mohamed Younis, Halabi Hasbullah, Application-centric connectivity restoration algorithm for wireless sensor and actor networks grid and pervasive computing. pp. 243- 253 ,(2011) , 10.1007/978-3-642-20754-9_25
Shehla Riaz, Hamra Afzaal, Muhammad Imran, Nazir Ahmad Zafar, Mehmet Sabih Aksoy, None, Formalizing Mobile Ad Hoc and Sensor Networks Using VDM-SL☆ Procedia Computer Science. ,vol. 63, pp. 148- 153 ,(2015) , 10.1016/J.PROCS.2015.08.325
Gerrit Jan Tretmans, Automatic Testing with Formal Methods CTIT technical report series. ,(1999)
Muhammad Imran, Mohamed Younis, Abas Md Said, Halabi Hasbullah, Volunteer-instigated connectivity restoration algorithm for Wireless Sensor and Actor Networks wireless communications, networking and information security. pp. 679- 683 ,(2010) , 10.1109/WCINS.2010.5544679
Muhammad Imran, Nazir Ahmad Zafar, Formal Specification and Validation of a Hybrid Connectivity Restoration Algorithm for Wireless Sensor and Actor Networks Sensors. ,vol. 12, pp. 11754- 11781 ,(2012) , 10.3390/S120911754
Mohammed Alnuem, Nazir Ahmad Zafar, Muhammad Imran, Sana Ullah, Mahmoud Fayed, Formal Specification and Validation of a Localized Algorithm for Segregation of Critical/Noncritical Nodes in MAHSNs International Journal of Distributed Sensor Networks. ,vol. 10, pp. 140973- ,(2014) , 10.1155/2014/140973
Jinglin Du, Li Xie, Xiaoyan Sun, Ruoqin Zheng, Application-Oriented Fault Detection and Recovery Algorithm for Wireless Sensor and Actor Networks International Journal of Distributed Sensor Networks. ,vol. 8, pp. 273792- ,(2012) , 10.1155/2012/273792
A. Abbasi, M. Younis, U. Baroudi, Restoring Connectivity in Wireless Sensor-Actor Networks with Minimal Topology Changes international conference on communications. pp. 1- 5 ,(2010) , 10.1109/ICC.2010.5502448