Novel abstraction methods for TDMA based MAC protocols: Case of IIoT MAC Wireless HART Verification

N. Suresh Kumar (), G. Santhosh Kumar (), S. Shailesh () and A. Sreekumar ()
Additional contact information
N. Suresh Kumar: Cochin University of Science and Technology
G. Santhosh Kumar: Cochin University of Science and Technology
S. Shailesh: Cochin University of Science and Technology
A. Sreekumar: Cochin University of Science and Technology

Telecommunication Systems: Modelling, Analysis, Design and Management, 2024, vol. 85, issue 1, No 8, 125-150

Abstract: Abstract All Internet of Things application layer protocols are built on top of the Medium Access Control layer (MAC layer). The MAC Layer’s primary goal is to limit or eliminate packet collisions. The technique of checking a protocol’s behavior that is represented by formal models is known as formal verification. Model checkers are used by protocol developers to automate the formal verification process because the human procedure of formal verification requires a great deal of mathematical concepts. This method uses model specification language to create formal models for the formal verification of protocols. The formal models’ temporal claims are used to specify the properties that need to be proved. If the property provided using temporal claims is not satisfied, the model checker uses these formal model and temporal claims and outputs a violating trace. There are only a few works that support the formal verification of MAC protocols. It’s because their behavior is difficult to abstract using model specification language. This paper suggests new abstraction methods in the form of algorithms for designing and modeling Time Division Multiple Access (TDMA) based scheduled MAC protocol using model specification language. Modeling links, superframes, multiple superframes, device schedules, and TDMA protocol abstraction are among the methods proposed. In order to support the applicability of the proposed methods, a TDMA-based formal model that meets the Wireless Highway Addressable Remote Transducer protocol specification requirements was created using PROMELA, a model specification language for SPIN model checker. In normal and constrained channel environments, the reachability of various marked states added into the model using temporal claims is verified. The verification result shows that the protocol performs as expected in a non-lossy channel environment. However, the protocol exhibits reliability issues due to message loss in a constrained channel environment. Finally, the model is checked for errors in design and message collisions. The results of the verification show that the model is free of design flaws and message collisions. The abstraction schemes proposed in this work help to quickly develop formal models for the verification of TDMA-based scheduled MAC protocols using model-checking tools.

Keywords: Formal verification; Internet of Things; PROMELA; Protocol verification; SPIN model checker; Wireless HART (search for similar items in EconPapers)
Date: 2024
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
http://link.springer.com/10.1007/s11235-023-01069-3 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:telsys:v:85:y:2024:i:1:d:10.1007_s11235-023-01069-3

Ordering information: This journal article can be ordered from
http://www.springer.com/journal/11235

DOI: 10.1007/s11235-023-01069-3

Access Statistics for this article

Telecommunication Systems: Modelling, Analysis, Design and Management is currently edited by Muhammad Khan

More articles in Telecommunication Systems: Modelling, Analysis, Design and Management from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().