论文标题
用自旋模型检查器分析弗雷托斯调度行为
Analyzing FreeRTOS Scheduling Behaviors with the Spin Model Checker
论文作者
论文摘要
Freertos是一个实时操作系统，具有可配置的调度策略。它的可移植性和可配置性使得Freertos成为嵌入式设备最受欢迎的实时操作系统之一。我们在这项工作中正式分析了ARM Cortex-M4处理器上的Freertos调度程序。具体来说，我们为Freertos Arm Cortex-M4端口构建了一个正式模型，并应用模型检查以在我们的Freertos示例应用程序中找到错误。有趣的是，在不同的调度策略下，在我们的应用模型中发现了几个错误。为了确认我们的发现，我们修改了由Freertos分发的申请程序，并在STM32F429I-DISC1董事会上复制断言失败。
FreeRTOS is a real-time operating system with configurable scheduling policies. Its portability and configurability make FreeRTOS one of the most popular real-time operating systems for embedded devices. We formally analyze the FreeRTOS scheduler on ARM Cortex-M4 processor in this work. Specifically, we build a formal model for the FreeRTOS ARM Cortex-M4 port and apply model checking to find errors in our models for FreeRTOS example applications. Intriguingly, several errors are found in our application models under different scheduling policies. In order to confirm our findings, we modify application programs distributed by FreeRTOS and reproduce assertion failures on the STM32F429I-DISC1 board.
