Building Design Artifacts for Formal Modeling and Verification of IoT Protocols

Abstract

The Internet has been utilized by billions of users in recent years, for everything from basic web page viewing to intricate corporate transactions. newlineTypically, a computer terminal, laptop, or smartphone is the endpoint device utilized for communication in each of these cases. Today, it is possible newlineto transfer computing and communication capabilities to every real-world newlinephysical thing . These things can now be linked to the Internet through newlineIPV6 that are equipped with sensors and actuators. Sensors measure tangible parameters from the objects and communicate this information to a newlinecollector node. The actuators perform triggering of some actions based on newlinethe value read by the sensor. The term Internet of Things (IoT) was suggested for such systems by Kevin Ashton in 1999 while integrating RFID newlinechips in the products to track the supply chain of Procter and Gamble. IoT newlinedevices are typically power-constrained and need power optimization to newlineimprove their life span. The development of the Internet of Things (IoT) newlinehas highly affected many areas of human life. The Internet of Medical newlineThings, the Industrial Internet of Things, the Internet of Flying Things, the newlineInternet of Floating Things, and the Internet of Autonomous Things are newlinerecent evolutions of IoT. In this thesis, methodologies to develop formal specifications and external behavior covering the basic behavior of IoT protocols, TDMA MAC protocols, and communication environment in Underwater Sensor Networks are proposed. The artifacts built from the suggested newlinemethodologies are generic ensuring reuse. Hence the contribution of this newlinethesis sets a path to the protocol developers to easily adapt to the formal newlinemodeling and verification from specification. newline newline