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

TL;DR

This paper presents a Spin-based model checking approach for verifying simple concurrent programs on preemptive RTOS, demonstrating automatic verification of race conditions, starvation, and deadlocks in a Linux-like kernel environment.

Contribution

It adapts an existing RTOS scheduling model to Spin, enabling automatic verification and applying it to real-world kernel designs and architectures.

Findings

No race conditions detected in the tested kernel model

The model confirms absence of deadlocks under preemptive scheduling

Verification process is automated and efficient

Abstract

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 verified rather than formulating proofs by hand. Moreover, we look into the designs of a Linux-like real-time kernel--Piko/RT and the specification of ARMv7-M architecture to reconstruct the model, and use LTL to specify a simple concurrent programs--consumer/producer problem during the development stage of the kernel. We show that under the preemptive scheduling and the mechanism of ARMv7-M, the program will not suffer from race condition, starvation, and deadlock.