| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2009-03-12 15:15 モデル検査ツールUPPAALを用いたGALSシステムの形式的検証 ○桐田和明・横川智教・宮崎 仁・佐藤洋一郎・早瀬道芳（岡山県立大）  VLD2008-150 |
|
| 抄録 | （和） | GALS (Globally Asynchronous Locally Synchronous)システムの設計では， 設計したシステムが意図した通りに動作することを検証する必要がある． GALSシステムは非同期通信を行うため，検証を行うには連続時間性を考慮してモデル化しなければならない． しかし，従来の検証手法ではこの点が十分に考慮されていなかった． 本研究では，連続時間に基づく検証ツールUPPAALを用いて，GALSシステムの設計を形式的に検証する手法を提案している． STPN (Stochastic Timed Petri Nets)でモデル化されたGALSシステムを， UPPAALで扱う拡張時間オートマトンに変換する手法を提案し，ツールとして実装している． 適用例として，STPNで記述されたGALSシステムに提案法を適用して検証を行い，手法の有効性を確認している． |
| （英） | To design GALS (Globally Asynchronous Locally Synchronous) systems, it is necessary to verify the correctness of behavior of the system formally. To verify asynchronous systems such as the GALS systems, the systems need to be modeled as continuous time systems. The previous methods to verify GALS systems formally, however, modeled the systems in discrete time. In this paper, we propose a method to verify a design of GALS system using model checker UPPAAL which employs continuous time. We propose a method to translate STPN (Stochastic Timed Petri Nets) model which represents a GALS system into extended Timed Automata and implement the proposed method. Finally, we show the availability of the proposed method by applying it to an STPN which models a GALS system. |
|
| キーワード | （和） | GALSシステム / STPN / UPPAAL / モデル検査 / 時間オートマトン / / / |
| （英） | GALS systems / STPN / UPPAAL / model checking / timed automaton / / / | |
| 文献情報 | 信学技報, vol. 108, no. 478, VLD2008-150, pp. 141-146, 2009年3月. | |
| 資料番号 | VLD2008-150 | |
| 発行日 | 2009-03-04 (VLD) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | VLD2008-150 |
|
| 研究会情報 | |
| 研究会 | VLD |
| 開催期間 | 2009-03-11 - 2009-03-13 |
| 開催地（和） | 沖縄県男女共同参画センター |
| 開催地（英） | |
| テーマ（和） | システムオンシリコンを支える設計技術 |
| テーマ（英） | Design Technology for a System-on-Silicon |
| 講演論文情報の詳細 | |
| 申込み研究会 | VLD |
| 会議コード | 2009-03-VLD |
| 本文の言語 | 日本語 |
| タイトル（和） | モデル検査ツールUPPAALを用いたGALSシステムの形式的検証 |
| サブタイトル（和） | |
| タイトル（英） | Formal verification of GALS system designs using UPPAAL |
| サブタイトル（英） | |
| キーワード(1)（和/英） | GALSシステム / GALS systems |
| キーワード(2)（和/英） | STPN / STPN |
| キーワード(3)（和/英） | UPPAAL / UPPAAL |
| キーワード(4)（和/英） | モデル検査 / model checking |
| キーワード(5)（和/英） | 時間オートマトン / timed automaton |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 桐田 和明 / Kazuaki Kirita / キリタ カズアキ |
| 第1著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Pref. Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 横川 智教 / Tomoyuki Yokogawa / ヨコガワ トモユキ |
| 第2著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Pref. Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 宮崎 仁 / Hisashi Miyazaki / ミヤザキ ヒサシ |
| 第3著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Pref. Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 佐藤 洋一郎 / Yoichiro Sato / サトウ ヨウイチロウ |
| 第4著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Pref. Univ.) |
| 第5著者 氏名（和/英/ヨミ） | 早瀬 道芳 / Michiyoshi Hayase / ハヤセ ミチヨシ |
| 第5著者 所属（和/英） | 岡山県立大学 (略称： 岡山県立大) Okayama Prefectural University (略称： Okayama Pref. Univ.) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2009-03-12 15:15:00 |
| 発表時間 | 25分 |
| 申込先研究会 | VLD |
| 資料番号 | VLD2008-150 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | no.478 |
| ページ範囲 | pp.141-146 |
| ページ数 | 6 |
| 発行日 | 2009-03-04 (VLD) |
[研究会発表申込システムのトップページに戻る]