講演名 2011-03-11
モデル検査を用いたプログラムにおける再現性の低い潜在的欠陥の抽出手法 : データベースロック問題の検証
青木 善貴, 松浦 佐江子,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 我々はモデル検査手法を用いて稀有な条件で発生する不具合を発見する手法「モデル検査を用いたプログラムにおける再現性の低い潜在的欠陥の抽出手法」を提案してきた.今回この手法を用い制御フロー及びロック機能に着目してモデル化することにより,業務システムにおけるデータベースロック不具合の現象をとらえ,不具合原因の検証を行う,検査対象はERPソフトウェアであるSAPR/3のアドオンプログラムである.
抄録(英) We have proposed a method for detecting unusual latent defects in enterprise system using model checking techniques. Such unusual defects are difficult to detect by reviewing and testing the source code alone. We have verified the phenomenon and cause of database lock defect by creating a model from a control flow and a lock function, using proposed method. The target program is written in ABAP which is an add-on programming language for developing SAP R/3 which is ERP software.
キーワード(和) モデル検査 / バグ / UPPAAL / 抽象化
キーワード(英) Model Checking / Bug / UPPAAL / Abstraction
資料番号 KBSE2010-60
発行日

研究会情報
研究会 KBSE
開催期間 2011/3/3(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Knowledge-Based Software Engineering (KBSE)
本文の言語 JPN
タイトル(和) モデル検査を用いたプログラムにおける再現性の低い潜在的欠陥の抽出手法 : データベースロック問題の検証
サブタイトル(和)
タイトル(英) A Method for Detecting Unusual Latent Defects in Enterprise System Using Model Checking Techniques : Verification of Database Lock Problem
サブタイトル(和)
キーワード(1)(和/英) モデル検査 / Model Checking
キーワード(2)(和/英) バグ / Bug
キーワード(3)(和/英) UPPAAL / UPPAAL
キーワード(4)(和/英) 抽象化 / Abstraction
第 1 著者 氏名(和/英) 青木 善貴 / Yoshitaka Aoki
第 1 著者 所属(和/英) 芝浦工業大学大学院電気電子情報工学専攻
Graduate School of Engineering, Shibaura institute of technology Department of electronic engineering and computer science
第 2 著者 氏名(和/英) 松浦 佐江子 / Saeko Matsuura
第 2 著者 所属(和/英) 芝浦工業大学システム理工学部電子情報システム学科
Shibaura institute of technology Department of electronic information system College of Systems Engineering and Science
発表年月日 2011-03-11
資料番号 KBSE2010-60
巻番号(vol) vol.110
号番号(no) 468
ページ範囲 pp.-
ページ数 6
発行日