Skip to Main content Skip to Navigation
Journal articles

Formal Validation of a Deterministic MAC Protocol

Karen Godary-Dejean 1 David Andreu 2
1 EXPLORE - Robotique mobile pour l'exploration de l'environnement
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
2 DEMAR - Artificial movement and gait restoration
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier, CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This article deals with the formal validation of a medium access protocol. This protocol has been designed to meet the specific requirements of an implantable network-based neuroprosthese. This article presents the modeling of STIMAP with Time Petri Nets (TPN), and the verification of the deterministic medium access it provides, using timed model checking. Doing so, we show that existent formal methods and tools are not perfectly suitable for the validation of real system, espe- cially when some hardware parameters has to be considered. This article then presents how these difficulties have been managed and gives the validation results for STIMAP, providing constraints on the protocol parameters that must be respected to guaranty its determinism.
Complete list of metadata
Contributor : Karen Godary-Dejean <>
Submitted on : Thursday, March 29, 2012 - 2:07:03 PM
Last modification on : Monday, October 5, 2020 - 2:17:21 PM
Long-term archiving on: : Wednesday, December 14, 2016 - 6:34:48 PM


Files produced by the author(s)



Karen Godary-Dejean, David Andreu. Formal Validation of a Deterministic MAC Protocol. ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 12 (1), pp.N/A. ⟨10.1145/2406336.2406342⟩. ⟨lirmm-00679892v2⟩



Record views


Files downloads