| 講演名 | 2013-03-14 開発現場を想定したモデル検査に基づくプログラムの不具合検証 : 検査支援ツールを用いた安定的な検査(一般) 青木 善貴, 松浦 佐江子, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 開発現場では不十分な要件定義や実装時のミス・誤解等により人手では発見困難な不具合が発生する.担当する要員により原因特定にかかる工数が著しく違うことは,開発プロジェクトを計画通りに進捗させる妨げになるため不具合原因を安定的に特定できる手法が必要である.本研究ではモデル検査の非決定性を利用してソースコードのモデル化を行い,制御フローに関する不具合原因の特定を行う.今回,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 / Defect / UPPAAL / eclipse |
| 資料番号 | KBSE2012-69 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 2013/3/7(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 開発現場を想定したモデル検査に基づくプログラムの不具合検証 : 検査支援ツールを用いた安定的な検査(一般) |
| サブタイトル（和） | |
| タイトル（英） | Verification of Program Defects Based on Model Checking Techniques for Development : Stable Checking with Inspection Support Tool |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | 不具合 / Defect |
| キーワード(3)（和/英） | UPPAAL / UPPAAL |
| キーワード(4)（和/英） | eclipse / eclipse |
| 第 1 著者 氏名（和/英） | 青木 善貴 / Aoki Yoshitaka |
| 第 1 著者 所属（和/英） | 日本ユニシス株式会社:芝浦工業大学大学院工学研究科 Nihon Unisys, Ltd. |
| 第 2 著者 氏名（和/英） | 松浦 佐江子 / Matsuura Saeko |
| 第 2 著者 所属（和/英） | 芝浦工業大学大学院工学研究科 hibaura institute of technology Department of electronic information system College of Systems Engineering and Science |
| 発表年月日 | 2013-03-14 |
| 資料番号 | KBSE2012-69 |
| 巻番号（vol） | vol.112 |
| 号番号（no） | 496 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |