The development of embedded applications (such as Wireless Sensor Network protocols) often requires a shift to formal specifications. To insure the reliability and the performance of the WSNs, such protocols must be designed following some methods reducing error rate. Formal methods (as Automata, Petri nets, algebra, logics, etc.) were largely used in the specification of these protocols, their analysis and their verification. After that, their implementation is an important phase to deploy, test and use those protocols in real environments. The main objective of the current paper is to formalize the transformation from high-level specification (in Timed Automata) to low-level implementation (in NesC language and TinyOs system) and to automate such transformation. The proposed transformation approach defines a set of rules that allow the passage between these two levels. We implemented our solution and we illustrated the proposed approach on a protocol case study for the" humidity" and" temperature" sensing in WSNs applications.