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.
Type de document :
Article dans une revue
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 12 (1), pp.N/A
Liste complète des métadonnées

https://hal-lirmm.ccsd.cnrs.fr/lirmm-00679892
Contributeur : Karen Godary-Dejean <>
Soumis le : jeudi 29 mars 2012 - 14:07:03
Dernière modification le : vendredi 12 janvier 2018 - 01:52:29
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 18:34:48

Fichier

TECS_tmp.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : lirmm-00679892, version 2

Citation

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. 〈lirmm-00679892v2〉

Partager

Métriques

Consultations de la notice

336

Téléchargements de fichiers

644