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

2011 年度 実施状況報告書

分散システムの振る舞いモデル自動合成のためのネット理論展開

研究課題

研究課題/領域番号 23500045
研究機関大阪大学

研究代表者

宮本 俊幸  大阪大学, 工学(系)研究科(研究院), 准教授 (00294041)

研究期間 (年度) 2011-04-28 – 2014-03-31
キーワードソフトウェア開発効率化・安定化 / ソフトウェア工学 / アルゴリズム / エージェント / 情報システム
研究概要

高信頼ソフトウェアの開発は,安心・安全な社会を実現する上で必要である.本研究では,分散システムにおけるモデルベースのソフトウェア開発を対象として,抽象的な要求仕様(シナリオ)から,分散システムを構成するモジュールの振る舞いモデル(状態機械図)を自動合成するための理論構築およびアルゴリズム開発を目的とする. 平成23年度では,シナリオから状態機械図を自動合成するために,ペトリネットからUMLの階層型状態機械図への変換方法を開発するための理論的考察を行った.ペトリネットの表現能力と状態機械図の表現能力の差により,任意のペトリネットを状態機械図に変換することは困難であった.そこで,平成23年度では,シナリオの数を単一と制限する事によって,ペトリネットから階層型状態機械図に変換可能であることを示した.また,その成果を電子情報通信学会のシステム数理と応用(MSS)研究会にて成果報告した. また,上記の議論を進めるためにUMLの部分集合であるcbUMLを提案した.cbUMLは,クラス,メッセージ,属性,コミュニケーション図,状態機械図から構成され,議論を進めるのに必要かつ十分なUMLの部分集合である.これにより,平成24年度以降に実施を予定しているアルゴリズムの開発およびその実装がスムーズに行えるようになった.cbUMLの定義および操作的意味をMSS研究会にて成果報告した. さらに,合成によって得られた状態機械図の動作検証を行うために,状態機械図をSMTソルバーを使ってモデル検査する方法,およびペトリネットをモジュラーモデル検査する手法を提案し,MSS研究会および国際会議(IEEE IECON 2011)にて成果報告した.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

平成23年度では,シナリオから状態機械図を自動合成するために,ペトリネットからUMLの階層型状態機械図への変換方法を開発するための理論的考察を行った.ペトリネットの表現能力と状態機械図の表現能力の差により,任意のペトリネットを状態機械図に変換することは困難であった.そこで,平成23年度では,シナリオの数を単一と制限する事によって,ペトリネットから階層型状態機械図に変換可能であることを示した. 研究計画では,平成23年度においては「シナリオー状態機械図変換のための理論的考察」を行うことになっており,おおむね研究計画通りに進展している.

今後の研究の推進方策

平成23年度の研究が順調に進んだため,当初計画通りに研究を推進していく. すなわち,平成24年度の前半に「シナリオー状態機械図変換アルゴリズム」を開発し,後半からアルゴリズムの実装に移る.平成25年度にかけて開発したアルゴリズムを定量的に評価する. 研究成果は順次国内外学会において成果報告していく.

次年度の研究費の使用計画

購入を予定していたソフトウェアを無償のソフトウェアに切り替えたため,平成23年度の研究費に未使用額が生じたが,平成24年度以降の旅費および論文別刷り費として使用する.

  • 研究成果

    (6件)

すべて 2012 2011

すべて 学会発表 (6件)

  • [学会発表] SMTソルバーを用いたUML状態機械の有界モデル検査に関する一考察2012

    • 著者名/発表者名
      新村 勇人
    • 学会等名
      電子情報通信学会システム数理と応用研究会
    • 発表場所
      高知市文化プラザかるぽーと(高知県)
    • 年月日
      2012年1月26日
  • [学会発表] cbUMLのコミュニケーション図から状態機械への変換およびそれらの形式的意味について2012

    • 著者名/発表者名
      長谷川 泰央
    • 学会等名
      電子情報通信学会システム数理と応用研究会
    • 発表場所
      高知市文化プラザかるぽーと(高知県)
    • 年月日
      2012年1月26日
  • [学会発表] ペトリネットを用いたサービス振る舞いモデルの自動合成2011

    • 著者名/発表者名
      宮本 俊幸
    • 学会等名
      電子情報通信学会ソサイエティ大会
    • 発表場所
      北海道大学(北海道)
    • 年月日
      2011年9月16日
  • [学会発表] ブリッジ除去による UML コミュニケーション図から UML 状態機械図への変換手法の正当性について2011

    • 著者名/発表者名
      長谷川 泰央
    • 学会等名
      第55回システム制御情報学会研究発表講演会
    • 発表場所
      大阪大学コンベンションセンター(大阪府)
    • 年月日
      2011年5月18日
  • [学会発表] Modular Reachability Analysis in Fundamental Class of Multi-agent Nets2011

    • 著者名/発表者名
      Toshiyuki Miyamoto
    • 学会等名
      IEEE IECON 2011
    • 発表場所
      クラウン国際会議場(メルボルン,オーストラリア)
    • 年月日
      2011年11月9日
  • [学会発表] SOAに基づくシステムの設計検証のためのUMLサブセット2011

    • 著者名/発表者名
      長谷川 泰央
    • 学会等名
      電子情報通信学会システム数理と応用研究会
    • 発表場所
      山口大学(山口県)
    • 年月日
      2011年11月18日

URL: 

公開日: 2013-07-10  

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

Powered by NII kakenhi