A Promela Model for Contiki’s Scheduler

摘要

This paper presents a formal model for the scheduler of Contiki, which is an event-driven lightweight Operating System for the Internet of Things (IoT). The proposed formal model enhances our knowledge regarding the most critical components of Contiki, namely its process and event queues, and its scheduler. We first derive a state machine-based abstraction of the scheduler’s modes of operation along with the control flow abstractions of the scheduler’s most important functions. We then use a set of transformation rules to generate the formal specifications of the scheduler in Promela. The generated Promela model enables simulation and verification of the scheduler in the SPIN model checker, which makes the proposed model a valuable artifact for researchers, educators and developers of Contiki. We also report on some design flaws we discovered during model extraction, simulation and verification. The contributions of this paper can readily be extended to other lightweight event-driven operating systems for Cyber Physical Systems (CPS) and IoT.