the reliability is of particular importance. On the other hand, due to the high interaction of the systems with hardware, how to manage interrupts, memory limitations and light weight of operations should be considered. One of the most used operating systems in this field is Contiki. In fact, Contiki is a lightweight, open source operating system in C. In addition, high portability and the ability to run on a variety of platforms and event-oriented features are also important features of Contiki. In this project, we have analyzed one of the most critical components of Contiki called the scheduling algorithm and then formally reviewed it. To this end, first we have analyzed the scheduling algorithm source code and also the interaction with other parts of the operating system in detail. Also, we have driven a state machine-based ion of the scheduler’s modes of operation along with the control flow ions of the scheduler’s most important functions. Meanwhile, in the current research, models of process, process list, event and event queue, which are the most important coordination structures of scheduling functions, are presented. We then have extracted a set of transformation rules to generate the formal specifications of the scheduler in Promela and accordingly, the Promela model is generated. After that, expected properties of the proper functionality of scheduler are analyzed and then converted into formal Linear Time Logic formulas. Finally, the formulas are applied to the Contiki scheduler algorithm using SPIN model checker and formally verified. As a result, in this project, three flaws were found in the Contiki’s scheduler and accordingly, the source code are fixed. Model Extraction، Formal Verification، Scheduler