| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2009-06-03 14:25 CPUと動的再構成可能プロセッサとの協調システムのモデル検査 ○南 翔太・瀧内新悟・瀬古口 智・山根 智（金沢大）  CST2009-3 |
|
| 抄録 | （和） | CPUとDRPが協調動作するような動的再構成可能組込みシステムのモデル化，仕様記述とモデル検査手法を提案する．プリエンプションやデッドラインのあるCPUはリアルタイムシステムとして仕様記述し，動作周波数の変化が生じるDRPはハイブリッドシステムとして仕様記述する．CPUとDRPを同時に検証しようとすると状態爆発が生じるため，(1)CPUを仕様記述したオートマトンと，環境及びDRPを抽象化したオートマトンとの並列合成オートマトンの検証，(2)DRPを仕様記述したオートマトンと，CPUを抽象化したオートマトンとの並列合成オートマトンの検証の2つの手順を踏むこで，システム全体の安全性を悲観的に検証する． |
| （英） | In this paper, we propose formal verification for cooperated systems consisting of CPU and DRP. First, we specify CPU as real-time systems and DRP as hybrid systems using hybrid automata. Next, we verify specifications using model cheking. In this process, we split the specifications into CPU side and DRP side to avoid state explosion. Our proposed techniques enables us to check safety properties such as schedulability conservatively. | |
| キーワード | （和） | 動的再構成可能プロセッサ(DRP) / モデル検査 / / / / / / |
| （英） | Dynamically Reconfigurable Processor(DRP) / Model checking / / / / / / | |
| 文献情報 | 信学技報, vol. 109, 2009年6月. | |
| 資料番号 | ||
| 発行日 | 2009-05-27 (CST) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | CST2009-3 |
|
| 研究会情報 | |
| 研究会 | MSS |
| 開催期間 | 2009-06-03 - 2009-06-04 |
| 開催地（和） | 摂南大学大阪センター |
| 開催地（英） | Setsunan University, Osaka Center |
| テーマ（和） | 【新型インフルエンザへの対応として中止を決定しました】ペトリネット，離散事象システム，一般 |
| テーマ（英） | Petri Net, Discrete Event System, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | MSS |
| 会議コード | 2009-06-CST |
| 本文の言語 | 日本語 |
| タイトル（和） | CPUと動的再構成可能プロセッサとの協調システムのモデル検査 |
| サブタイトル（和） | |
| タイトル（英） | Model checking of cooperated systems consisting of CPU and DRP |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 動的再構成可能プロセッサ(DRP) / Dynamically Reconfigurable Processor(DRP) |
| キーワード(2)（和/英） | モデル検査 / Model checking |
| キーワード(3)（和/英） | / |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 南 翔太 / Shota Minami / ミナミ ショウタ |
| 第1著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 瀧内 新悟 / Shingo Takinai / タキナイ シンゴ |
| 第2著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 瀬古口 智 / Satoshi Sekoguchi / セコグチ サトシ |
| 第3著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 山根 智 / Satoshi Yamane / ヤマネ サトシ |
| 第4著者 所属（和/英） | 金沢大学 (略称： 金沢大) Kanazawa University (略称： Kanazawa Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2009-06-03 14:25:00 |
| 発表時間 | 25分 |
| 申込先研究会 | MSS |
| 資料番号 | CST2009-3 |
| 巻番号（vol） | vol.109 |
| 号番号（no） | no.73 |
| ページ範囲 | pp.13-18 |
| ページ数 | 6 |
| 発行日 | 2009-05-27 (CST) |
[研究会発表申込システムのトップページに戻る]