Verification of the DMAMAC Protocol

DMAMAC Protocol is a Medium Access Control for process automation applications.

Firstly, the publications describing the DMAMAC protocol and the conducted model-based verification of the protocol are listed here. The source files for the Uppaal models created for the verification follows the list of articles.
  • K. Somappa, A. A., Ovsthus, K., & Kristensen, L., "Towards a Dual-Mode Adaptive MAC Protocol (DMA-MAC) for Feedback-based Networked Control Systems", in Proceedings of the 2nd International Workshop on Communications and Sensor Networks (ComSense), Procedia Computer Science, 34, pp. 505-510, 2014.(pdf) (Publication)
  • K. Somappa, A. A., Prinz, A., & Kristensen, L., "Model-Based Verification of the DMAMAC Protocol for Real-time Process Control",in Proceedings of the 9th International Workshop on Verification and Evaluation of Computer and Communication Systems , VECoS, 2015.(pdf) (Publication)

DMAMAC Uppaal Model

The Dual-Mode Adaptive Medium Access Control protocol (DMAMAC), designed to have two operational modes to cater for the two process control states. The protocol has a transient mode that supports the transient state, and a steady mode to support the steady state. The transient mode has data communication at a higher rate relative to the steady state. We designed DMAMAC for applications where steady state dominates the process operation. Teh DMAMAC protocol is designed for process control applications with real-time requirements. To increase our confidence on the design of the protocol, we have created a timed Uppaal model to verify the design. Below we have compiled the list of source files together with a readme on how to use all the files. We used Uppaal academic version 4.1.19 to conduct the verification. Part of this work has also been in a report for the course work IKT617 at University of Agder. The report is also attached below.
  • IKT617 report. (pdf)
  • Source files for different versions of the model. (zip)

Old Uppaal project

  • Ajith Kumar, "Adding Schedulability Analysis to the Octopus toolset," Master thesis Report, Embedded Systems Institute, Technical University of Eindhoven and Manipal University. (pdf)

(Last Updated Sep-05-2015)