Formal Validation of a Deterministic MAC Protocol - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Journal Articles ACM Transactions on Embedded Computing Systems (TECS) Year : 2012

Formal Validation of a Deterministic MAC Protocol

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.
Fichier principal
Vignette du fichier
TECSRevue_STIMAP.pdf (511.03 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

lirmm-00679892 , version 1 (16-03-2012)
lirmm-00679892 , version 2 (29-03-2012)

Identifiers

  • HAL Id : lirmm-00679892 , version 1

Cite

Karen Godary-Dejean, David Andreu. Formal Validation of a Deterministic MAC Protocol. ACM Transactions on Embedded Computing Systems (TECS), 2012, to appear. ⟨lirmm-00679892v1⟩
331 View
418 Download

Share

More