[2026年7月29日提出]

PDFを表示 HTML（実験的）

要約:リアルタイムオペレーティングシステム（RTOS）は、予測可能なタスク実行を実現するためにスケジューラの実装に依存しています。安全クリティカルシステムの場合、抽象的なスケジューリングポリシーだけでなく、具体的な実装が意図したスケジューリングセマンティクスを保持していることも必要です。特に最早期限優先（EDF）スケジューリングでは、動的で期限から導出される優先度が導入されるため、固定優先度スケジューリング用に設計されたカーネルインフラストラクチャを再利用して実現されることが多く、困難を伴います。本研究では、Earliest Deadline First（EDF）スケジューラの実装が満たすべき3つの必須特性を通じてEDFの正しさを形式化します。これらの特性に基づき、EDFベースのスケジューラ実装に適用可能な演繹的検証を利用したフレームワークを提案します。このフレームワークをFrama-C/ACSLで実装し、RTEMS 5、RTEMS 6、およびFreeRTOSのEDF拡張という3つの構造的に異なるEDFスケジューラ実装に適用しました。

提出履歴

差出人: Jian-Jia Chen [メールを表示]
[v1] 2026年7月29日（水）13:56:07 UTC (177 KB)