スピンモデルチェッカーによるFreeRTOSスケジューリング挙動の解析【JST・京大機械翻訳】

Lin Chen-Kai; Wang Bow-Yaw

プレプリント

J-GLOBAL ID：202202212977947369 整理番号：22P0350567

スピンモデルチェッカーによるFreeRTOSスケジューリング挙動の解析【JST・京大機械翻訳】

Analyzing FreeRTOS Scheduling Behaviors with the Spin Model Checker

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (2件)： ,
資料名：
発行年： 2022年05月16日プレプリントサーバーでの情報更新日： 2022年10月06日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

フリーRTOSは,構成可能なスケジューリング政策を有するリアルタイムオペレーティングシステムである。そのポータビリティと構成性は,組込みデバイスのための最も一般的なリアルタイムオペレーティングシステムのフリーRTOSを1つにする。本研究では,ARM Cortex-M4プロセッサ上のFreeRTOSスケジューラを形式的に解析した。具体的には,FreeRTOS ARM Cortex-M4ポートに対する形式的モデルを構築し,FreeRTOS例アプリケーションに対する著者らのモデルの誤差を見つけるためのモデル検査を適用した。興味深いことに,いくつかの誤差が,異なるスケジューリング政策の下で,著者らの応用モデルで見つかった。著者らの発見を確認するために,著者らは,FreeRTOSによって分布する応用プログラムを修正して,STM32F429I-DISC1ボードに関するアサーション故障を再現した。【JST・京大機械翻訳】

, , , , , ,
, , , 【Automatic Indexing@JST】

オペレーティングシステム

, ,

前のページに戻る