Formal Verification of a MAC Protocol for Underwater Sensor Networks
The use of Underwater Sensor Networks (UWSN) for underwater ocean applications such as seismic event detection, target detection, marine resource monitoring, and oil bed monitoring is growing. In contrast to conventional WSNs, these networks communicate via acoustic channels. Many communication prot...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2023-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10274980/ |
| _version_ | 1797658032020127744 |
|---|---|
| author | N. Suresh Kumar G. Santhosh Kumar Shailesh Sivan A. Sreekumar |
| author_facet | N. Suresh Kumar G. Santhosh Kumar Shailesh Sivan A. Sreekumar |
| author_sort | N. Suresh Kumar |
| collection | DOAJ |
| description | The use of Underwater Sensor Networks (UWSN) for underwater ocean applications such as seismic event detection, target detection, marine resource monitoring, and oil bed monitoring is growing. In contrast to conventional WSNs, these networks communicate via acoustic channels. Many communication protocols for UWSN have been proposed, including MAC layer protocols, time synchronization protocols, and routing protocols. Formal verification of these protocols is rarely investigated. In this paper, we propose two abstraction methods for UWSN that capture multi-channel models and variable propagation delay. These abstraction methods are used to create a validation model of the Time Delay Allocation MAC (TDA-MAC) protocol, which is used in UWSN. Formal verification of TDA-MAC is accomplished by performing a reachability analysis and the occurrence of design faults on certain marked states in the model. The verification results detect non-progress cycles of marked states in the event of a PING message loss. A modification to the existing protocol specification of TDA-MAC protocol is proposed. Formal verification on the refined validation model shows that the protocol is free from non-progress cycles and unreachable states. The proposed abstraction methods can be used to create formal models and perform formal verification of existing and emerging protocols used in UWSN. |
| first_indexed | 2024-03-11T17:53:15Z |
| format | Article |
| id | doaj.art-8a6d3de80e324041a1832864a48dfa9e |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-03-11T17:53:15Z |
| publishDate | 2023-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-8a6d3de80e324041a1832864a48dfa9e2023-10-17T23:00:32ZengIEEEIEEE Access2169-35362023-01-011111184611185910.1109/ACCESS.2023.332358510274980Formal Verification of a MAC Protocol for Underwater Sensor NetworksN. Suresh Kumar0https://orcid.org/0000-0002-2211-5058G. Santhosh Kumar1Shailesh Sivan2A. Sreekumar3Department of Computer Science, Cyber Physical Systems Laboratory, Cochin University of Science and Technology (CUSAT), Kochi, Kerala, IndiaDepartment of Computer Science, Cyber Physical Systems Laboratory, Cochin University of Science and Technology (CUSAT), Kochi, Kerala, IndiaDepartment of Computer Science, Cyber Physical Systems Laboratory, Cochin University of Science and Technology (CUSAT), Kochi, Kerala, IndiaDepartment of Computer Applications, Cochin University of Science and Technology (USAT), Kochi, Kerala, IndiaThe use of Underwater Sensor Networks (UWSN) for underwater ocean applications such as seismic event detection, target detection, marine resource monitoring, and oil bed monitoring is growing. In contrast to conventional WSNs, these networks communicate via acoustic channels. Many communication protocols for UWSN have been proposed, including MAC layer protocols, time synchronization protocols, and routing protocols. Formal verification of these protocols is rarely investigated. In this paper, we propose two abstraction methods for UWSN that capture multi-channel models and variable propagation delay. These abstraction methods are used to create a validation model of the Time Delay Allocation MAC (TDA-MAC) protocol, which is used in UWSN. Formal verification of TDA-MAC is accomplished by performing a reachability analysis and the occurrence of design faults on certain marked states in the model. The verification results detect non-progress cycles of marked states in the event of a PING message loss. A modification to the existing protocol specification of TDA-MAC protocol is proposed. Formal verification on the refined validation model shows that the protocol is free from non-progress cycles and unreachable states. The proposed abstraction methods can be used to create formal models and perform formal verification of existing and emerging protocols used in UWSN.https://ieeexplore.ieee.org/document/10274980/Formal verificationPROMELASPIN model checkerTDA-MACunderwater sensor networks (UWSN) |
| spellingShingle | N. Suresh Kumar G. Santhosh Kumar Shailesh Sivan A. Sreekumar Formal Verification of a MAC Protocol for Underwater Sensor Networks IEEE Access Formal verification PROMELA SPIN model checker TDA-MAC underwater sensor networks (UWSN) |
| title | Formal Verification of a MAC Protocol for Underwater Sensor Networks |
| title_full | Formal Verification of a MAC Protocol for Underwater Sensor Networks |
| title_fullStr | Formal Verification of a MAC Protocol for Underwater Sensor Networks |
| title_full_unstemmed | Formal Verification of a MAC Protocol for Underwater Sensor Networks |
| title_short | Formal Verification of a MAC Protocol for Underwater Sensor Networks |
| title_sort | formal verification of a mac protocol for underwater sensor networks |
| topic | Formal verification PROMELA SPIN model checker TDA-MAC underwater sensor networks (UWSN) |
| url | https://ieeexplore.ieee.org/document/10274980/ |
| work_keys_str_mv | AT nsureshkumar formalverificationofamacprotocolforunderwatersensornetworks AT gsanthoshkumar formalverificationofamacprotocolforunderwatersensornetworks AT shaileshsivan formalverificationofamacprotocolforunderwatersensornetworks AT asreekumar formalverificationofamacprotocolforunderwatersensornetworks |