講演名 2013-03-14
モデル検査を使ったデッドロック可能性検出(一般)
猿渡 卓也, 塚本 英昭, 神谷 慎吾, 宮田 俊介,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 形式手法の適用によるITシステムの信頼性向上が期待されている.しかし,形式手法の適用にはモデル作成等の専門的な知識が必要となるため,一般的な技術者によるシステム開発での適用の敷居は高い.本研究では,形式手法の一種であるモデル検査に必要なモデルの構築を容易に実施できるような手順を考案し,DBアクセスに伴うデッドロックの可能性箇所の検出を試みた.また,ケーススタディを実施し,考案した手順の有効性を確かめた.
抄録(英) Improvement of IT system's dependability using formal methods is expected. In a typical IT system development, formal methods are not much used. In this paper, we tried to use "model checking" that is one of the methods of formal method and detect potential deadlocks in DB access. At that time, we worked out the procedure that makes applying the model checking easy. In the procedure, we focus the purpose of model checking, and use simple notation for model checking. We conducted a case study and confirmed a validity of the procedure.
キーワード(和) デッドロック / 形式手法 / モデル検査 / DB / SPIN
キーワード(英) Deadlock / Formal method / Model checking / DB / SPIN
資料番号 KBSE2012-76
発行日

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

講演論文情報詳細
申込み研究会 Knowledge-Based Software Engineering (KBSE)
本文の言語 JPN
タイトル(和) モデル検査を使ったデッドロック可能性検出(一般)
サブタイトル(和)
タイトル(英) Model checking potential deadlocks of DB transactions
サブタイトル(和)
キーワード(1)(和/英) デッドロック / Deadlock
キーワード(2)(和/英) 形式手法 / Formal method
キーワード(3)(和/英) モデル検査 / Model checking
キーワード(4)(和/英) DB / DB
キーワード(5)(和/英) SPIN / SPIN
第 1 著者 氏名(和/英) 猿渡 卓也 / Takuya SARUWATARI
第 1 著者 所属(和/英) 日本電信電話株式会社ソフトウェアイノベーションセンタ
NTT, Software Innovation Center
第 2 著者 氏名(和/英) 塚本 英昭 / Hideaki TSUKAMOTO
第 2 著者 所属(和/英) 日本電信電話株式会社ソフトウェアイノベーションセンタ
NTT, Software Innovation Center
第 3 著者 氏名(和/英) 神谷 慎吾 / Shingo KAMIYA
第 3 著者 所属(和/英) 日本電信電話株式会社ソフトウェアイノベーションセンタ
NTT, Software Innovation Center
第 4 著者 氏名(和/英) 宮田 俊介 / Shunsuke MIYATA
第 4 著者 所属(和/英) 日本電信電話株式会社ソフトウェアイノベーションセンタ
NTT, Software Innovation Center
発表年月日 2013-03-14
資料番号 KBSE2012-76
巻番号(vol) vol.112
号番号(no) 496
ページ範囲 pp.-
ページ数 6
発行日