WEKO3
アイテム
有界モデル検査を用いたリアルタイムOSカーネルのタスク管理モジュールに対する形式的検証
https://ipsj.ixsq.nii.ac.jp/records/224560
https://ipsj.ixsq.nii.ac.jp/records/224560785f5555-0dfc-4d28-b316-4a6046619ffc
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SE23213020.pdf (905.3 kB)
|
Copyright (c) 2023 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2023-03-02 | |||||||||
| タイトル | ||||||||||
| タイトル | 有界モデル検査を用いたリアルタイムOSカーネルのタスク管理モジュールに対する形式的検証 | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | Formal Verification of Task Management Modules in Real-Time OS Kernels Using Bounded Model Checking | |||||||||
| 言語 | ||||||||||
| 言語 | jpn | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | 解析・検査・保護 | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||||
| 資源タイプ | technical report | |||||||||
| 著者所属 | ||||||||||
| 金沢大学 | ||||||||||
| 著者所属 | ||||||||||
| 金沢大学 | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Kanazawa Uniersity | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Kanazawa Uniersity | ||||||||||
| 著者名 |
小柴, 真之介
× 小柴, 真之介
× 山根, 智
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | 現在，組込みシステムの規模が著しく増加しており，組込みシステムにはリアルタイムオペレーティングシステム (RTOS) は必要不可欠である．RTOS は厳密な時間制約があり，時間制約の違反が重大な事故に繋がりかねない．時間制約を守るためにはタスクのスケジューリングの正当性が重要である．また，セマフォを使用したタスク間の排他制御ではタスクの優先度逆転現象 [1] が発生することがある．そこで，本論文では，TOPPERS[2] で公開されている RTOS を対象とし，C/C++ をフルサポートし，SAT/SMT solver に基づく CBMC[3] と呼ばれる既製の有界型モデル検査器を用いて RTOS のタスク管理モジュールに対する新しい検証手法を提案する．特にタスクのスケジューリング処理の正当性や優先度逆転現象の発生を形式的に検証できることができ，これによりシステムのスケジューリングの正当性が保証され，現実的な時間制約ミスの発見に有効である． | |||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | The scale of embedded systems is increasing significantly, and a real-time operating system (RTOS) is indispensable for embedded systems. RTOS has strict time constraints, and violation of time constraints can lead to serious accidents. Validity of task scheduling is important to keep time constraints. In addition, exclusion control between tasks using semaphores may cause task priority inversion. In this paper, we describe a new approach to verify task management modules in RTOS published by TOPPERS using an off-the-shelf bounded model checker called CBMC, which fully supports C/C++ and is based on SAT/SMT solver. In particular, it is able to formally verify the correctness of the task scheduling process and the occurrence of priority inversions, which guarantees the correctness of the system scheduling and is effective in detecting realistic time constraint errors. | |||||||||
| 書誌レコードID | ||||||||||
| 収録物識別子タイプ | NCID | |||||||||
| 収録物識別子 | AN10112981 | |||||||||
| 書誌情報 |
研究報告ソフトウェア工学（SE） 巻 2023-SE-213, 号 20, p. 1-8, 発行日 2023-03-02 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 2188-8825 | |||||||||
| Notice | ||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
