講演抄録/キーワード |
講演名 |
2015-03-05 14:30
モジュラ化手法によるモデル検査の検討とモジュラ検証の実用化 ○宮島卓巳(茨城大)・小飼 敬(茨城高専)・上田賀一(茨城大)・山形知行・武澤隆之(日立) KBSE2014-56 |
抄録 |
(和) |
検査対象を機械的かつ網羅的に探索するモデル検査は,探索範囲の指数的増加のため適用が困難である.そこで,検査対象を構造と振舞いの観点から結合度の低い箇所を分割することでモジュラ化を行い,別々に検証し,1回に探索する範囲を制限することでモデル検査の実用化を目指す.本研究では,列車運行システムにおいてモジュラ化の有無による実験結果を比較し,有効性を評価する. |
(英) |
Model checking to search mechanically and cyclopedically for inspection system is difficult because of exponential increase of the search area. Therefore, we divide target model to modules from the view-point of the structure and behavior. And we aim at practical use of the model checking by verifying a module separately. This study shows the comparison of modular method and non-modula by using a train operation system as the subject of evaluation experiment. |
キーワード |
(和) |
モデル検査 / SPIN / 状態爆発 / モジュラ検証 / / / / |
(英) |
model checking / SPIN / state explosion / modular verification / / / / |
文献情報 |
信学技報, vol. 114, no. 501, KBSE2014-56, pp. 25-30, 2015年3月. |
資料番号 |
KBSE2014-56 |
発行日 |
2015-02-26 (KBSE) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
KBSE2014-56 |