| 講演名 | 2002/11/21 並行周期EFSMに対するパラメトリックモデル検査およびパラメタ条件簡約高速化の一手法 舛田 文彦, 森 亮憲, 中田 明夫, 東野 輝夫, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | パラメトリックモデル検査は,与えられた状態遷移モデルがある性質を満たすためのパラメタ条件を導出する手法である.本論文では,並行周期EFSMに対するパラメトリックモデル検査手法を提案する.検証する性質は実時間拡張CTL(RPCTL)で記述する.周期EFSMとはEFSMの実時間拡張の一種であり,ある一定時間(周期)が経過すると初期状態へ戻るようなモデルである.提案手法では,並行周期EFSMをオンザフライ(on-the-fly)で単一周期EFSMに変換し,パラメタ条件を導出する.パラメタ条件WPC(s,f)は,状態sで性質fが満たされるための条件式を表し,部分条件WPC(s_i,f_i)を再帰的に計算することによって導出する.部分条件WPC(s_i,f_i)を計算する際,条件式に含まれる限定子の消去および条件式の簡約をオンザフライで行う.更に,部分条件WPC(s_i,f_i)の結果が条件WPC(s,f)に影響を及ぼさない場合は部分条件の計算を省略し計算時間を短縮する. |
| 抄録(英) | In this paper, we develop a parametric model checking method for concurrent periodic EFSMs and a property described in a real-time extension of CTL(RPCTL). The periodic EFSM is a kind of a real-time extension of the EFSM model that after some constant period T has elapsed, it returns to its initial state. In the proposed method, the concurrent periodic EFSMs are translated into a single periodic EFSM on-the-fly, and the parameter condition is derived. The parameter condition WPC(s, f), in order that the state s satisfies the property f. is derived by recursively computing the subconditions WPC(s_i, f_i) for its next states s_i and their derived properties f_i. We also introduce some optimization heuristics, such as the quantifier elimination of the derived formula. |
| キーワード(和) | パラメトリックモデル検査 / 実時間システム / 周期EFSM / 時相論理 / 限定子消去 |
| キーワード(英) | parametric model checking / real-time systems / periodic EFSMs / temporal logic / quantifier elimination |
| 資料番号 | VLD2002-89 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2002/11/21(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 並行周期EFSMに対するパラメトリックモデル検査およびパラメタ条件簡約高速化の一手法 |
| サブタイトル（和） | |
| タイトル（英） | Parametric Model Checking of Concurrent Periodic EFSMs and an Efficient Simplification Method of Parameter Conditions |
| サブタイトル（和） | |
| キーワード(1)（和/英） | パラメトリックモデル検査 / parametric model checking |
| キーワード(2)（和/英） | 実時間システム / real-time systems |
| キーワード(3)（和/英） | 周期EFSM / periodic EFSMs |
| キーワード(4)（和/英） | 時相論理 / temporal logic |
| キーワード(5)（和/英） | 限定子消去 / quantifier elimination |
| 第 1 著者 氏名（和/英） | 舛田 文彦 / Fumihiko MASUDA |
| 第 1 著者 所属（和/英） | 大阪大学大学院基礎工学研究科 Graduate School of Engineering Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 森 亮憲 / Takanori MORI |
| 第 2 著者 所属（和/英） | 大阪大学大学院基礎工学研究科 Graduate School of Engineering Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 中田 明夫 / Akio NAKATA |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 4 著者 氏名（和/英） | 東野 輝夫 / Teruo HIGASHINO |
| 第 4 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2002/11/21 |
| 資料番号 | VLD2002-89 |
| 巻番号（vol） | vol.102 |
| 号番号（no） | 476 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |