• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

有界モデル検査による仕様検証手法を利用したソフトウェア開発コストの削減

研究課題

研究課題/領域番号 19700030
研究種目

若手研究(B)

配分区分補助金
研究分野 ソフトウエア
研究機関岡山県立大学

研究代表者

横川 智教  岡山県立大学, 情報工学部, 助教 (50382362)

研究期間 (年度) 2007 – 2008
研究課題ステータス 完了 (2008年度)
配分額 *注記
3,620千円 (直接経費: 3,200千円、間接経費: 420千円)
2008年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
2007年度: 1,800千円 (直接経費: 1,800千円)
キーワードソフトウェア / モデル検査 / 有界モデル検査 / UML(Unified Modeling Language) / 形式手法 / 自動検証 / ソフトウェア工学 / UML(Unified Modeling Language
研究概要

本研究課題では,動的性質の検証手法であるモデル検査を用いたUML設計群の検証手法について研究開発を行った.本研究では特に,ソフトウェアの各モジュールの動作とモジュール間のメッセージ通信に関する設計の整合性に注目しており,各モジュールが与えられたメッセージ通信仕様を満たすか有界モデル検査により検証するものである.また,UML設計群を一つのモデルに統合することによるモデルの巨大化に伴い,検証コストが指数的に増大することが予想されるため,有界モデル検査の適用とその効率化についても研究を行っている.
この目的を達成するため,まず,モジュールの動作並びにモジュール間のメッセージ通信を記述するUML設計群から有界モデル検査のためのモデルを抽出する手法について研究開発を行った.各UML設計で記述された動的振る舞いを論理式表現し,それらを組み合わせることで有界モデル検査による検証を実現する.次に,有界モデル検査をUML設計群の検証に最適化するため,状態空間の探索アルゴリズムの比較実験を行った.また,適用実験の一環として,Webページのナビゲーション構造の検証についても研究開発を行い,UMLの状態マシン図によりモデル化されたナビゲーション構造をモデル検査により検証する手法について研究開発を行った.最後に,提案する検証系を計算機上に実装するため,与えられたUML設計群から論理式表現を自動生成するツールを開発した.
その成果として,UML設計群として与えられたモジュールの動作並びにモジュール間のメッセージ通信が互いに矛盾なく記述されているかを有界モデル検査により検証する枠組みを実現するとともに,自動検証ツールについて実装の一部を完了した.また,適用実験として,Webナビゲーション構造の設計に対して提案法による検証を行い,有効性を確認した.

報告書

(3件)
  • 2008 実績報告書   研究成果報告書 ( PDF )
  • 2007 実績報告書
  • 研究成果

    (21件)

すべて 2009 2008 2007

すべて 学会発表 (21件)

  • [学会発表] SMVを用いたUML設計の整合性検証ツールの作成2009

    • 著者名/発表者名
      原田慎士
    • 学会等名
      電機情報通信学会2009年総合大会
    • 発表場所
      愛媛大学
    • 年月日
      2009-03-17
    • 関連する報告書
      2008 実績報告書
  • [学会発表] 状態マシン図によるWebサイトのナビゲーション構造のモデル化2009

    • 著者名/発表者名
      宮崎仁
    • 学会等名
      ソフトウェア信頼性研究会第5回ワークショップ
    • 発表場所
      和歌山大学サテライト
    • 年月日
      2009-03-07
    • 関連する報告書
      2008 実績報告書
  • [学会発表] 記号モデル検査によるUML設計間の整合性検証2009

    • 著者名/発表者名
      宮崎仁
    • 学会等名
      ソフトウェア信頼性研究会第5回ワークショップ
    • 発表場所
      和歌山大学サテライト
    • 年月日
      2009-03-06
    • 関連する報告書
      2008 実績報告書
  • [学会発表] 記号モデル検査を用いた複数種のUML図設計間の整合性の検証2009

    • 著者名/発表者名
      宮崎仁
    • 学会等名
      ウインターワークショップ・イン・宮崎
    • 発表場所
      宮崎観光ホテル
    • 年月日
      2009-01-24
    • 関連する報告書
      2008 実績報告書
  • [学会発表] 状態マシン図を用いた動的なWebナビゲーションのモデル化2009

    • 著者名/発表者名
      瀬古剛一
    • 学会等名
      ウインターワークショップ・イン・宮崎
    • 発表場所
      宮崎観光ホテル
    • 年月日
      2009-01-24
    • 関連する報告書
      2008 実績報告書
  • [学会発表] A Tool Support for Verifying Consistency between UML Diagrams by SMV2009

    • 著者名/発表者名
      S. HARADA, T. YOKOGAWA, H. MIYAZAKI, Y. SATO, and M. HAYASE,
    • 学会等名
      In The 24th International Technical Conference on Circuits/Systems
    • 発表場所
      Computers and Communications (ITC-CSCC2009)
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] SMVを用いたUML設計の整合性検証ツールの作成,(ISS-P-136)2009

    • 著者名/発表者名
      原田慎士, 横川智教, 宮崎仁, 佐藤洋一郎, 早瀬道芳
    • 学会等名
      電子情報通信学会2009年総合大会ISS特別企画学生ポスターセッション
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 記号モデル検査によるUML設計間の整合性検証(27-34)2009

    • 著者名/発表者名
      宮崎仁, 横川智教, 佐藤洋一郎, 早瀬道
    • 学会等名
      ソフトウェア信頼性研究会第5回ワークショップ(FORCE2009)論文集
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 状態マシン図によるWebサイトのナビゲーション構造のモデル化(67-73)2009

    • 著者名/発表者名
      瀬古剛一, 横川智教, 宮崎仁, 佐藤洋一郎, 早瀬道芳
    • 学会等名
      ソフトウェア信頼性研究会第5回ワークショップ(FORCE2009)論文集
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 記号モデル検査を用いた複数種のUML図設計間の整合性の検証(79-80)2009

    • 著者名/発表者名
      宮崎仁, 横川智教,佐藤洋一郎, 早瀬道芳
    • 学会等名
      ウインターワークショップ2009・イン・宮崎論文集
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 状態マシン図を用いた動的なWebナビゲーションのモデル化(2009(3))2009

    • 著者名/発表者名
      瀬古剛一, 横川智教, 宮崎仁, 佐藤洋一郎, 早瀬道芳
    • 学会等名
      ウインターワークショップ2009・イン・宮崎論文集
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 記号モデル検査を用いた状態マシン図とシーケンス図の無矛盾性の検証2008

    • 著者名/発表者名
      宮崎仁
    • 学会等名
      情報処理学会ソフトウェア工学研究会
    • 発表場所
      岡山県立大学
    • 年月日
      2008-09-26
    • 関連する報告書
      2008 実績報告書
  • [学会発表] Formal Verification of Web Navigation by Symbolic Model Checking2008

    • 著者名/発表者名
      H. MIYAZAKI
    • 学会等名
      The 23rd International Technical Conference on Circuits/Systems, Computers and Communications ITC-CSCC2008)
    • 発表場所
      山口県下関市海峡メッセ
    • 年月日
      2008-07-07
    • 関連する報告書
      2008 実績報告書
  • [学会発表] 記号モデル検査を用いたWebナビゲーションの形式的検証2008

    • 著者名/発表者名
      瀬古 剛一
    • 学会等名
      電子情報通信学会2008年総合大会
    • 発表場所
      北九州学術研究都市
    • 年月日
      2008-03-18
    • 関連する報告書
      2007 実績報告書
  • [学会発表] 有界モデル検査を用いた複数UML図の形式的検証2008

    • 著者名/発表者名
      宮崎 仁
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 発表場所
      長崎大学
    • 年月日
      2008-03-03
    • 関連する報告書
      2007 実績報告書
  • [学会発表] Formal Verification of Web Navigation by Symbolic Model Checking(397-340)2008

    • 著者名/発表者名
      H. MIYAZAKI, T. YOKOGAWA, K. SEKO, Y. SATO, and M. HAYASE
    • 学会等名
      In The 23rd International Technical Conference on Circuits/Systems
    • 発表場所
      Computers and Communications (ITC-CSCC2008)
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 記号モデル検査を用いた状態マシン図とシーケンス図の無矛盾性の検証(2008-SE-16,41-47)2008

    • 著者名/発表者名
      宮崎仁, 横川智教, 瀬古剛一, 佐藤洋一郎, 早瀬道芳
    • 学会等名
      情報処理学会研究報告
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 有界モデル検査を用いた複数UML図の形式的検証(107(505, SS2007-59),13-18)2008

    • 著者名/発表者名
      宮崎仁, 横川智教, 瀬古剛一, 佐藤洋一郎, 早瀬道芳
    • 学会等名
      電子情報通信学会技術研究報告
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 記号モデル検査を用いたWebナビゲーションの形式的検証(ISS-P-145)2008

    • 著者名/発表者名
      瀬古剛一, 横川智教, 佐藤洋一郎, 早道芳
    • 学会等名
      電子情報通信学会2008年総合大会ISS特別企画学生ポスターセッション
    • 関連する報告書
      2008 研究成果報告書
  • [学会発表] 複数のUML図を対象とした記号モデル検査による形式的検証手法の提案2007

    • 著者名/発表者名
      佐藤 貞仁
    • 学会等名
      ソフトウェア信頼性研究会第4回ワークショップ
    • 発表場所
      愛媛大学
    • 年月日
      2007-06-08
    • 関連する報告書
      2007 実績報告書
  • [学会発表] 複数のUML図を対象とした記号モデル検査による形式的検証手法の提案(69-77)2007

    • 著者名/発表者名
      佐藤貞仁,宮崎仁,横川智教, 佐藤洋一郎, 早瀬道芳,
    • 学会等名
      ソフトウェア信頼性研究会第4回ワークショップ(FORCE2007)論文集
    • 関連する報告書
      2008 研究成果報告書

URL: 

公開日: 2007-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi