WEKO3
インデックスリンク
アイテム
Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata
http://hdl.handle.net/2297/6708
http://hdl.handle.net/2297/670888319aa0-ee13-4a1f-92d2-14dfa80640c4
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
TE-PR-YAMANE-S-527.pdf (735.5 kB)
|
|
| Item type | 会議発表論文 / Conference Paper(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2017-10-03 | |||||
| タイトル | ||||||
| タイトル | Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata | |||||
| 言語 | ||||||
| 言語 | eng | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||
| 資源タイプ | conference paper | |||||
| 著者 |
Yamane, Satoshi
× Yamane, Satoshi |
|||||
| 書誌情報 |
Proceedings - IEEE Computer Society's International Computer Software and Applications Conference p. 527-533, 発行日 2003-01-01 |
|||||
| ISSN | ||||||
| 収録物識別子タイプ | ISSN | |||||
| 収録物識別子 | 0730-6512 | |||||
| 出版者 | ||||||
| 出版者 | Institute of Electrical and Electronics Engineers (IEEE) | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | Real-time software runs over real-time operating systems, and guaranteeing Qualities is difficult. As timing constraints and resource allocations are strict, it is necessary to verify schedulability, safety and liveness properties. In this paper, we formally specify real-time software using hybrid automata and verify its schedulability using both deductive refinement theory and scheduling theory. In this case, the above real-time software consists of periodic processes and a fixed-priority preemptive scheduling policy on one CPU. Using our proposed methods, we can uniformally and easily specify real-time software and verify its schedulability based on hybrid automata. Moreover, we can verify its schedulability at design stage. | |||||
| 著者版フラグ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
