文献

J-GLOBAL ID：201002215416316316   整理番号：10A0979474

情報制御システム記述モデルの検証用記述への変換と効率的検証

著者 (6件)： 柳翔太 (茨城大) ,  小飼敬 (茨城工高専) ,  上田賀一 (茨城大) ,  大久保訓 (日立) ,  高橋勇喜 (日立) ,  中野利彦 (日立)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 27th  ページ： ROMBUNNO.7C-1  発行年： 2010年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ソフトウェア品質を確保する手法に形式検証を上げることができる。しかし,実践レベルへの形式検証の適用は多くの問題を抱えている。本研究では,情報制御システムを対象とし,専用の記述言語で記述されたモデルに対する実用的な検証の実行方法について検討する。一般に,モデル検証はモデル検査ツールを使用することで実行されるため,以下の3点について検討する。まず,対象モデルを検証用記述に変換する必要があるが,変換には専門の知識が必要となり現場での運用が難しい。そのため,検証用記述への変換ルールを定義する。次に,検証の実行をサポートするために,設計した検証項目をLTL式に変換する必要があり,その変換ルールを定義する。最後に,モデル検査では対象モデルの状態数が多いと実用的な範囲の時間で検証が実行できない場合がある。そのため,状態数を抑えるための工夫について検討する。モデルから検証用記述への変換方法とLTLへの変換方法を定義し,実用化のための工夫を施した結果,効率的なモデルの検証を行うことができた。(著者抄録)

シソーラス用語： *形式的手法【計算機】 ,  検証 ,  *情報システム ,  システム記述言語 ,  *モデル検査 ,  プログラム変換 ,  効率化
準シソーラス用語： 形式検証 ,  *情報制御システム

分類 (2件)： 計算理論  (JB02000A) ,  その他の情報処理  (JE15050M)

タイトルに関連する用語 (4件)： 情報制御システム ,  記述 ,  モデル ,  検証