In the context of distributed systems, the communication requirements are very different depending on the supported application, the system topology and the environment. The functional electrical stimulation is a critical and real time application domain: communications have to be safe (no loss, neither long nor unexpected delay). Therefore, an important part of this system from an efficiency point of view is the medium access mechanism. To fit with the specific constraints of our context, a new MAC protocol has been designed: STIMAP (Sliding Time Interval based Medium Access Protocol). This article presents a formal validation of this new protocol, allowing the validation of its behavior in an exhaustive way.