| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2007-08-03 11:45 UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法 ○長岡武志・岡野浩三・楠本真二（阪大）  SS2007-29 |
|
| 抄録 | （和） | 近年，情報システムの高信頼設計においてモデル検査は重要な役割を果たすようになってきている．実時間システムのモデル検査では，モデルの状態数が状態変数やクロック変数に対して指数的に増加し，スケーラビリティに厳しい制限が生じる．本稿では，時間モデル検査ツールであるUPPAALで用いられる拡張時間オートマトンに対する具体的なモデル抽象化手法を提案する．モデル抽象化技法はこのスケーラビリティ改善のための主要な手法として注目を浴びている．本手法では，Clarkeらが提案した反例に基づいた抽象化改良ループCEGARを適用しており，抽象化から検査までの全ての工程を自動的に行うことが可能である． |
| （英） | In the model checking of the realtime systems, the number of states of models increases exponentlly with the number of the state variables and the clock variables. Such explosion severely limits the scalability of model checking. This paper proposes a concrete model abstraction technique for extended timed automata used in UPPAAL, a famous model checking tool for realtime systems.In the proposed technique, the abstraction refinement loop based on the counterexample that Clarke et al. proposed is applied, and all the processes from the abstraction can be performed automatically.We gives concrete procedures for the abstraction loop with utilization of DBM. | |
| キーワード | （和） | モデル検査 / 時間オートマトン / モデル抽象化 / CEGAR / UPPAAL / / / |
| （英） | Model Checking / Timed Automata / Model Abstraction / CEGAR / UPPAAL / / / | |
| 文献情報 | 信学技報, vol. 107, no. 176, SS2007-29, pp. 77-82, 2007年8月. | |
| 資料番号 | SS2007-29 | |
| 発行日 | 2007-07-26 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2007-29 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2007-08-02 - 2007-08-03 |
| 開催地（和） | 北海道大学 |
| 開催地（英） | Hokkaido Univ. |
| テーマ（和） | 一般 |
| テーマ（英） | general |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2007-08-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法 |
| サブタイトル（和） | |
| タイトル（英） | Abstraction of Extended Timed Automata for UPPAAL Based on Counterexample-Guided Abstraction Refinement Loop |
| サブタイトル（英） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | 時間オートマトン / Timed Automata |
| キーワード(3)（和/英） | モデル抽象化 / Model Abstraction |
| キーワード(4)（和/英） | CEGAR / CEGAR |
| キーワード(5)（和/英） | UPPAAL / UPPAAL |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 長岡 武志 / Takeshi Nagaoka / ナガオカ タケシ |
| 第1著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ) |
| 第2著者 氏名（和/英/ヨミ） | 岡野 浩三 / Kozo Okano / オカノ コウゾウ |
| 第2著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ) |
| 第3著者 氏名（和/英/ヨミ） | 楠本 真二 / Shinji Kusumoto / クスモト シンジ |
| 第3著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ) |
| 講演者 | 第1著者 |
| 発表日時 | 2007-08-03 11:45:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2007-29 |
| 巻番号（vol） | vol.107 |
| 号番号（no） | no.176 |
| ページ範囲 | pp.77-82 |
| ページ数 | 6 |
| 発行日 | 2007-07-26 (SS) |
[研究会発表申込システムのトップページに戻る]