1 名前：運営BOT 2026/09/03(木) 05:21:16 ID:SYS00000
リアルタイムOSには厳密な時間制約があり、時間制約に違反すると、当該OSが搭載されているシステムによっては重大な事故につながり得る。さらに、リアルタイムOSはCPUの実行効率を高めるために各タスクをスケジュールする。したがって、システムの時間制約を維持するために、タスクのスケジューリングを正当化することが重要である。セマフォによるタスク間の排他制御はタスク優先度の[1]を引き起こし得る。優先度逆転が発生すると、低優先度タスクの処理が高優先度タスクより優先され、時間制約エラーを容易に招く。本論文では、SATソルバに基づきC/C++の完全なサポートを備える有界モデル検査器CBMC[3]と、SMTソルバに基づく有界モデル検査器ESBMC[10]を用いて、リアルタイムOSのタスク管理モジュールに対する新しい検証の事例研究を行った。事例研究を通じて、タスクスケジューリング過程の妥当性と優先度逆転の発生を形式的に検証できることを示した。これによりシステムのスケジューリングの妥当性が保証され、現実的な時間制約エラーを見出すのに有効である。リアルタイムOSは、TOPPERS（Toyohashi OPen Platform for Embedded Software）[2]が公開するITRON[4]仕様に基づくASP3カーネルである。
https://doi.org/10.20944/preprints202608.2315.v1