| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2013-09-12 13:15 割り込み処理に着目した組込みソフトウェアへのモデル検査適用の検討 ○佐々木隆益（電通大）・吉岡信和（NII）・田原康之・大須賀昭彦（電通大）  KBSE2013-39 |
|
| 抄録 | （和） | 組み込み製品において，不適切な割り込み処理による不具合をテストで検出するのは再現性がなく困難である．これに関しては，モデル検査技術による解決の可能性がある．しかしながら，割り込みのようなハードウェアに依存したシステムにおけるモデル検査の効率的でかつ実践可能な手法の提案は少ない．本研究では，ハードウェアを含めたシステムモデリングの必要性を明らかにし，Promelaによる割り込みのフレームワークを提案する．また提案手法を用いることで，ハードウェアやモデル検査について熟知していない一般ソフトウェアエンジニアでも，効率的にハードウェアを含めたシステムのモデル検査が可能なことをARPプロトコルの振る舞いに適用し確認した． |
| （英） | Detecting errors from incorrect interrupt processing when testing embedded systems is difficult because same scenario can not be reproduced. It is possible to resolve the problem using Model Checking. However there are not enough researches to suggest that Model Checking is effective and practical for hardware-dependent systems. In this paper, we clarify the necessity of the system modeling including hardware and propose the framework of interrupt processing designed by Promela language. This method was applied for ARP protocol behavior and confirmed that it is able to execute the Model Checking effectively for the software engineers who don’t know the hardware systems and model checking. | |
| キーワード | （和） | モデル検査 / Promela / SPIN / 割り込み / / / / |
| （英） | Model Checking / Promela / SPIN / Interrupt Processing / / / / | |
| 文献情報 | 信学技報, vol. 113, no. 215, KBSE2013-39, pp. 19-24, 2013年9月. | |
| 資料番号 | KBSE2013-39 | |
| 発行日 | 2013-09-05 (KBSE) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | KBSE2013-39 |
|
| 研究会情報 | |
| 研究会 | KBSE |
| 開催期間 | 2013-09-12 - 2013-09-13 |
| 開催地（和） | 電気通信大学 |
| 開催地（英） | The University of Electro-Communications |
| テーマ（和） | 一般 |
| テーマ（英） | Genaral session |
| 講演論文情報の詳細 | |
| 申込み研究会 | KBSE |
| 会議コード | 2013-09-KBSE |
| 本文の言語 | 日本語 |
| タイトル（和） | 割り込み処理に着目した組込みソフトウェアへのモデル検査適用の検討 |
| サブタイトル（和） | |
| タイトル（英） | A Study of the Application of Model Checking to Embedded Software Based on Interrupt Processing |
| サブタイトル（英） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | Promela / Promela |
| キーワード(3)（和/英） | SPIN / SPIN |
| キーワード(4)（和/英） | 割り込み / Interrupt Processing |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 佐々木 隆益 / Takanori Sasaki / ササキ タカノリ |
| 第1著者 所属（和/英） | 電気通信大学 (略称： 電通大) University of Electro-Communications (略称： UEC) |
| 第2著者 氏名（和/英/ヨミ） | 吉岡 信和 / Nobukazu Yoshioka / ヨシオカ ノブカズ |
| 第2著者 所属（和/英） | 国立情報学研究所 (略称： NII) National Institute of Informatics (略称： NII) |
| 第3著者 氏名（和/英/ヨミ） | 田原 康之 / Yasuyuki Tahara / タハラ ヤスユキ |
| 第3著者 所属（和/英） | 電気通信大学 (略称： 電通大) University of Electro-Communications (略称： UEC) |
| 第4著者 氏名（和/英/ヨミ） | 大須賀 昭彦 / Akihiko Ohsuga / オオスガ アキヒコ |
| 第4著者 所属（和/英） | 電気通信大学 (略称： 電通大) University of Electro-Communications (略称： UEC) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第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著者 |
| 発表日時 | 2013-09-12 13:15:00 |
| 発表時間 | 35分 |
| 申込先研究会 | KBSE |
| 資料番号 | KBSE2013-39 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | no.215 |
| ページ範囲 | pp.19-24 |
| ページ数 | 6 |
| 発行日 | 2013-09-05 (KBSE) |
[研究会発表申込システムのトップページに戻る]