A Spin-based model checking for the simple concurrent program on a preemptive RTOS

Chen-Kai Lin, Ching-Chun, Huang +1

We adapt an existing preemptive scheduling model of RTOS kernel by eChronos from machine-assisted proof to Spin-based model checker. The model we constructed can be automatically v…