講演抄録/キーワード |
講演名 |
2013-03-14 15:30
モデル検査を使ったデッドロック可能性検出 ○猿渡卓也・塚本英昭・神谷慎吾・宮田俊介(NTT) KBSE2012-76 |
抄録 |
(和) |
形式手法の適用による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 / / / |
文献情報 |
信学技報, vol. 112, no. 496, KBSE2012-76, pp. 43-48, 2013年3月. |
資料番号 |
KBSE2012-76 |
発行日 |
2013-03-07 (KBSE) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
KBSE2012-76 |