電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
技報オンライン
‥‥ (ESS/通ソ/エレソ/ISS)
技報アーカイブ
‥‥ (エレソ/通ソ)
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 2009-03-12 15:15
モデル検査ツールUPPAALを用いたGALSシステムの形式的検証
桐田和明横川智教宮崎 仁佐藤洋一郎早瀬道芳岡山県立大
技報オンラインサービス実施中
抄録 (和) 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

研究会情報
研究会 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著者 所属(和/英) (略称: )
(略称: )
第19著者 氏名(和/英/ヨミ) / /
第19著者 所属(和/英) (略称: )
(略称: )
第20著者 氏名(和/英/ヨミ) / /
第20著者 所属(和/英) (略称: )
(略称: )
講演者
発表日時 2009-03-12 15:15:00 
発表時間 25 
申込先研究会 VLD 
資料番号 IEICE-VLD2008-150 
巻番号(vol) IEICE-108 
号番号(no) no.478 
ページ範囲 pp.141-146 
ページ数 IEICE-6 
発行日 IEICE-VLD-2009-03-04 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会