Implementation of Spin-based checking for preemptive RTOS scheduling behavior: the case study of Piko/RT

  • 林 振凱

Student thesis: Master's Thesis


Formal verification is used to guarantee that under the hardware and software specification the target system must not behave unexpectedly With the various applications of the ICT product those unexpected behaviors might cause different degrees of losses Formal verification is one way to claim that good properties will happen eventually and bad properties will never happen in the target system Piko/RT is a tiny real-time operating system kernel ptimized for the Internet of Things With the massive growth of IOT network “safety” and “stable” are the most significant issue In this study we apply model checking method on a new RTOS kernel to verify its scheduling behavior without affecting the development of the kernel With this method we can increase the chance to find unexpected behaviors which are less obvious by unit tests and code review We design an abstract scheduling model from the hardware and software aspects including the preemptive scheduling and exception behavior of the ARMv7-M Architecture And claims that mutex and condition variable have no mutual exclusion and deadlock under the specific situation
Date of Award2018 Feb 14
Original languageEnglish
SupervisorSheng-Tzong Cheng (Supervisor)

Cite this