IDEAS home Printed from https://ideas.repec.org/a/spr/telsys/v85y2024i1d10.1007_s11235-023-01069-3.html
   My bibliography  Save this article

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

Author

Listed:
  • 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)

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.

Suggested Citation

  • N. Suresh Kumar & G. Santhosh Kumar & S. Shailesh & A. Sreekumar, 2024. "Novel abstraction methods for TDMA based MAC protocols: Case of IIoT MAC Wireless HART Verification," Telecommunication Systems: Modelling, Analysis, Design and Management, Springer, vol. 85(1), pages 125-150, January.
    • Handle: RePEc:spr:telsys:v:85:y:2024:i:1:d:10.1007_s11235-023-01069-3
    DOI: 10.1007/s11235-023-01069-3
    as

    Download full text from publisher

    File URL: http://link.springer.com/10.1007/s11235-023-01069-3
    File Function: Abstract
    Download Restriction: Access to the full text of the articles in this series is restricted.
    File URL: https://libkey.io/10.1007/s11235-023-01069-3?utm_source=ideas
    LibKey link: if access is restricted and if your library uses this service, LibKey will redirect you to where you can use your library subscription to access this item
    ---><---

    As the access to this document is restricted, you may want to search for a different version of it.

    References listed on IDEAS

    as
    1. Luiz Oliveira & Joel J. P. C. Rodrigues & Sergei A. Kozlov & Ricardo A. L. Rabêlo & Victor Hugo C. de Albuquerque, 2019. "MAC Layer Protocols for Internet of Things: A Survey," Future Internet, MDPI, vol. 11(1), pages 1-42, January.
    Full references (including those not matched with items on IDEAS)

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Mohammad Mansour & Amal Gamal & Ahmed I. Ahmed & Lobna A. Said & Abdelmoniem Elbaz & Norbert Herencsar & Ahmed Soltan, 2023. "Internet of Things: A Comprehensive Overview on Protocols, Architectures, Technologies, Simulation Tools, and Future Directions," Energies, MDPI, vol. 16(8), pages 1-39, April.
    2. Abdallah Y. Alma’aitah & Mohammad A. Massad, 2021. "Reader–Tag Commands via Modulation Cutoff Intervals in RFID Systems," Future Internet, MDPI, vol. 13(9), pages 1-13, September.
    3. Georgios Tsoumanis & Asterios Papamichail & Vasileios Dragonas & George Koufoudakis & Constantinos T. Angelis & Konstantinos Oikonomou, 2020. "Implementation of a Topology Independent MAC (TiMAC) Policy on a Low-Cost IoT System," Future Internet, MDPI, vol. 12(5), pages 1-13, May.
    4. Nikolaos Schizas & Aristeidis Karras & Christos Karras & Spyros Sioutas, 2022. "TinyML for Ultra-Low Power AI and Large Scale IoT Deployments: A Systematic Review," Future Internet, MDPI, vol. 14(12), pages 1, December.

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:spr:telsys:v:85:y:2024:i:1:d:10.1007_s11235-023-01069-3. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Sonal Shukla or Springer Nature Abstracting and Indexing (email available below). General contact details of provider: http://www.springer.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.