基于自旋的抢占式RTOS上简单并发程序的模型检验
A Spin-based model checking for the simple concurrent program on a preemptive RTOS
摘要：
我们通过eChronos将现有的RTOS内核抢占式调度模型从机器辅助证明修改为基于Spin的模型检查器。我们构建的模型可以自动验证，而不是用手工证明。此外，我们还研究了一个类似Linux的实时内核--Piko/RT的设计和ARMv7-M体系结构的规范来重建模型，并在内核开发阶段使用LTL来描述一个简单的并发程序--消费者/生产者问题。我们证明了在抢占式调度和ARMv7-M机制下，程序不会出现竞争条件、饥饿和死锁。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
