| 講演名 | 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 |
| 発行日 | |