| 講演名 | 1997/7/16 抽象実行によるnon-Zenoな実時間システムの公平性の形式的検証 山根 智, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 時間オートマトンの検証では, 公平性の扱いは難しい. なぜならば, 閉ループであってもタイミング制約により, 無限に実行されないことがあるためである. 一方, 抽象実行の一種である近似解法により, 時間オートマトンの効率的な到達可能解析手法が開発されている. 従来の研究では, 時間オートマトンの効率的な公平性の検証手法が提案されていない. 本論文では, 時間オートマトンにおける公平性の記述の条件を明確にして, 時間不等式手法と二分決定グラフを結合した近似解法による時間オートマトンの言語包含検証方式を提案する. |
| 抄録(英) | It is difficult to verify fairness in timed automata, because in some cases, timed automata can not behave infinitely often even if there is some closed cyle. On the other hand, effective formal verification based on abstract interpretation has been developed. But we can not verify fairness in timed automata by existing methods. In this paper, we proposed formal verification of fairness in timed automata based on abstract interpretation, which combine BDDs with DBMs. |
| キーワード(和) | 時間オートマトン / 抽象実行 / 二分決定グラフ / 形式的検証 |
| キーワード(英) | Timed Automata / Abstract Interpretation / BDDs / Formal Verification |
| 資料番号 | SS97-17 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1997/7/16(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 抽象実行によるnon-Zenoな実時間システムの公平性の形式的検証 |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification of Fairness for non-Zeno Real-Time Systems by Abstract Interpretation |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 時間オートマトン / Timed Automata |
| キーワード(2)（和/英） | 抽象実行 / Abstract Interpretation |
| キーワード(3)（和/英） | 二分決定グラフ / BDDs |
| キーワード(4)（和/英） | 形式的検証 / Formal Verification |
| 第 1 著者 氏名（和/英） | 山根 智 / Satoshi Yamane |
| 第 1 著者 所属（和/英） | 島根大学総合理工学部数理・情報システム学科計算機科学講座 Dept. of Mathematics and Computer Science, Shimane University |
| 発表年月日 | 1997/7/16 |
| 資料番号 | SS97-17 |
| 巻番号（vol） | vol.97 |
| 号番号（no） | 164 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |