| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2013-03-14 10:05 開発現場を想定したモデル検査に基づくプログラムの不具合検証 ～ 検査支援ツールを用いた安定的な検査 ～ ○青木善貴（日本ユニシス）・松浦佐江子（芝浦工大）  KBSE2012-69 |
|
| 抄録 | （和） | 開発現場では不十分な要件定義や実装時のミス・誤解等により人手では発見困難な不具合が発生する.担当する要員により原因特定にかかる工数が著しく違うことは，開発プロジェクトを計画通りに進捗させる妨げになるため不具合原因を安定的に特定できる手法が必要である．本研究ではモデル検査の非決定性を利用して，ソースコードを順次モデル化することにより不具合原因の特定を行う．今回，Javaのソースコードを対象にし，eclipseのプラグインを用いたモデル検査支援ツールを用意した．このツールは指示されたステートメントの取り扱いに従いソースコードを検査モデルに変換する．この検査モデルを検査することにより安定した不具合原因の特定が行える． |
| （英） | In the development site, difficult defects of detecting occurs when Miss inadequate requirements definition and implementation. Changing of Man-hour for a person in charge interfere with the progress of development projects. Method is required to identify the cause of stable defects. In this study, we use a non-deterministic of model checking. Then we detect the cause of defect by modeling the source code sequence. This time, we were the subject of modeling the source code of Java. We were prepared to support model checking tool that consists of a plug-in eclipse. This tool will convert the source code to the checking model in accordance with the handling of the statements that have been indicated. We identify the cause of detects was can be done stably by examining this model. |
|
| キーワード | （和） | モデル検査 / UPPAAL / eclipse / バグ / / / / |
| （英） | Model Checking / UPPAAL / eclipse / bug / / / / | |
| 文献情報 | 信学技報, vol. 112, no. 496, KBSE2012-69, pp. 1-6, 2013年3月. | |
| 資料番号 | KBSE2012-69 | |
| 発行日 | 2013-03-07 (KBSE) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | KBSE2012-69 |
|
| 研究会情報 | |
| 研究会 | KBSE |
| 開催期間 | 2013-03-14 - 2013-03-15 |
| 開催地（和） | 芝浦工業大学 |
| 開催地（英） | Shibaura Institute of Technology |
| テーマ（和） | 一般 |
| テーマ（英） | General session |
| 講演論文情報の詳細 | |
| 申込み研究会 | KBSE |
| 会議コード | 2013-03-KBSE |
| 本文の言語 | 日本語 |
| タイトル（和） | 開発現場を想定したモデル検査に基づくプログラムの不具合検証 |
| サブタイトル（和） | 検査支援ツールを用いた安定的な検査 |
| タイトル（英） | Verification of Program Defects Based on Model Checking Techniques for Development |
| サブタイトル（英） | Stable Checking with Inspection Support Tool |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | UPPAAL / UPPAAL |
| キーワード(3)（和/英） | eclipse / eclipse |
| キーワード(4)（和/英） | バグ / bug |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 青木 善貴 / Yoshitaka Aoki / アオキ ヨシタカ |
| 第1著者 所属（和/英） | 日本ユニシス株式会社 (略称： 日本ユニシス) Nihon Unisys, Ltd (略称： Nihon Unisys) |
| 第2著者 氏名（和/英/ヨミ） | 松浦 佐江子 / Saeko Matsuura / |
| 第2著者 所属（和/英） | 芝浦工業大学 (略称： 芝浦工大) Shibaura Institute of Technology (略称： Shibaura Inst. of Tech.) |
| 講演者 | 第1著者 |
| 発表日時 | 2013-03-14 10:05:00 |
| 発表時間 | 35分 |
| 申込先研究会 | KBSE |
| 資料番号 | KBSE2012-69 |
| 巻番号（vol） | vol.112 |
| 号番号（no） | no.496 |
| ページ範囲 | pp.1-6 |
| ページ数 | 6 |
| 発行日 | 2013-03-07 (KBSE) |
[研究会発表申込システムのトップページに戻る]