文献

J-GLOBAL ID：201402279654705999   整理番号：14A1307222

情報制御システムにおける段階的検査法を用いたモジュラ検証

著者 (5件)： 宮島卓巳 (茨城大) ,  小飼敬 (茨城工高専) ,  上田賀一 (茨城大) ,  山形知行 (日立) ,  武澤隆之 (日立)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 31st  ページ： ROMBUNNO.IPPAN1-4  発行年： 2014年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： モデル検査は検査対象の振舞いモデルを機械的かつ網羅的に探索を行うことで,仕様通り振舞うか検査する手法である。しかし,実践的なモデルに対しモデル検査を適用する場合,状態爆発が発生する可能性が高い。本研究では,検査対象のシステムをいくつかのサブシステムに分割して検証するモジュラ検証を段階的検査法を用いて実現する。サブシステムごとに分割してモデル化を行い,それぞれ他モデルの状態を入力として与えながら段階的検査法を適用し,領域間の横断に加え,モデル間の横断を改めて繋ぐことでモデル検査を行う。これにより検証モデル内の状態数を削減でき,状態空間の肥大化を防ぐことができる。本研究では,列車運行システムにおいて段階的手法のみ適用の場合とモジュラ検証した場合の比較を行い,有効性を評価する。(著者抄録)

シソーラス用語： 情報システム ,  制御装置 ,  *モデル検査 ,  性質 ,  *モジュール構造 ,  組合せ問題 ,  分割法 ,  モデリング ,  探索問題 ,  プログラム検査
準シソーラス用語： *モジュラ性 ,  情報制御システム ,  状態爆発問題 ,  列車運行制御システム

分類 (2件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (4件)： 情報制御システム ,  段階 ,  検査 ,  検証