Résumé
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.