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

2016 年度 実施状況報告書

非近似的アプローチによるリアクティブシステム仕様の効率的な実現可能性判定法

研究課題

研究課題/領域番号 15K15969
研究機関東京工業大学

研究代表者

島川 昌也  東京工業大学, 情報理工学院, 助教 (00749161)

研究期間 (年度) 2015-04-01 – 2018-03-31
キーワードリアクティブシステム仕様 / 実現可能性 / ω-オートマトン
研究実績の概要

リアクティブシステム仕様の実現可能性に関する検証は,仕様記述において見過ごされがちな危険な状況に陥る可能性を検出することができるが,一般に煩雑で計算コストの高い処理を伴う.本研究ではリアクティブシステム仕様の実現可能性検証の効率化を目的とし,本年度は以下について取り組んだ.

<on-the-fly簡約手法>:リアクティブシステム仕様の実現可能性検証においては,仕様から決定性ωオートマトンを構成する必要がある.近似を行わない場合,その手続は煩雑でコストが高い.模倣関係や強連結成分情報を利用し,ωオートマトンを簡約する手法について多く研究されている.それらの多くは,構成後のオートマトンに対して適用されるものである.本研究では,構成途中に簡約を適用することで扱う状態やエッジを減らし,構成自体のコストも低減させるon-the-fly簡約について検討する.本年度は,決定性ωオートマトン構成時に状態にラベルされる情報を利用して簡約を行う手法の開発を進めた.

<分割検証法>:分割検証とは,次のようなものである.i)分割されたそれぞれの部分仕様において決定性ωオートマトンを構成する.ii)各部分オートマトンにおいて局所的な情報を捨象する.iii)各部分オートマトンを統合し,解析する.このような検証では,ii)において局所的な情報を捨象できるため,一括検証に比べて高速に判定を行える.本年度においては,効率的な分割検証を行うための仕様の分割方法を提案した.

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

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

理由

on-the-fly簡約手法や分割検証法について検討し,一定の成果が得られた.それゆえ,現在までの進捗状況はおおむね順調であると判断した.

今後の研究の推進方策

これまでに提案してきた効率化手法を織り込んだ実現可能性判定器の実装を行う予定である.また,これまでの研究成果を整理し,様々な形で公表していく予定である.

次年度使用額が生じた理由

国際会議・国内学会の参加費・旅費,及び英文校正費用にあてる予定であった分が学内予算でまかなえたため,次年度使用額が生じた.

次年度使用額の使用計画

開発・実験を行う上で必要となるPC周辺機器を購入する予定である.残りは当初の計画通り,国際会議・国内学会の参加費・旅費,及び英文校正費用等にあてる予定である.

  • 研究成果

    (8件)

すべて 2017 2016

すべて 雑誌論文 (1件) (うち査読あり 1件) 学会発表 (7件) (うち国際学会 5件)

  • [雑誌論文] Safraless LTL synthesis considering maximal realizability2016

    • 著者名/発表者名
      Takashi Tomita, Atsushi Ueno, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki
    • 雑誌名

      Acta Informatica

      巻: - ページ: 1-38

    • DOI

      10.1007/s00236-016-0280-3

    • 査読あり
  • [学会発表] Discussion on Verification of Voting Protocols2017

    • 著者名/発表者名
      Shigeki Hagihara, Masaya Shimakawa, Naoki Yonezaki
    • 学会等名
      Philippine Computing Science Congress (PCSC 2017)
    • 発表場所
      フィリピン
    • 年月日
      2017-03-16 – 2017-03-18
  • [学会発表] Combining Unification and Rewriting in Proofs for Modal Logics with First-order Undefinable Frames2017

    • 著者名/発表者名
      Shigeki Hagihara, Masahiko Tomoishi, Masaya Shimakawa, Naoki Yonezaki
    • 学会等名
      International Conference on Computer Science, Electronics Technology and Automation (ICCSETA 2017)
    • 発表場所
      中国
    • 年月日
      2017-03-11 – 2017-03-12
    • 国際学会
  • [学会発表] Modularization of formal specifications for efficient synthesis of reactive systems2017

    • 著者名/発表者名
      Masaya Shimakawa, Kenji Osari, Shigeki Hagihara, Naoki Yonezaki
    • 学会等名
      International Conference on Software and Computer Applications (ICSCA 2017)
    • 発表場所
      タイ
    • 年月日
      2017-02-26 – 2017-02-28
    • 国際学会
  • [学会発表] Web server access trend analysis based on the Poisson distribution2017

    • 著者名/発表者名
      Shigeki Hagihara, Yoshiharu Fushihara, Masaya Shimakawa, Masahiko Tomoishi, Naoki Yonezaki
    • 学会等名
      International Conference on Software and Computer Applications (ICSCA 2017)
    • 発表場所
      タイ
    • 年月日
      2017-02-26 – 2017-02-28
    • 国際学会
  • [学会発表] リアクティブシステム仕様の実現可能性に関する非有界検査の効率化に向けて(ポスター発表)2016

    • 著者名/発表者名
      島川昌也,萩原茂樹,米崎直樹
    • 学会等名
      第14回 ディペンダブルシステムワークショップ (DSW 2016)
    • 発表場所
      函館
    • 年月日
      2016-12-14 – 2016-12-15
  • [学会発表] Discussion of LTL Subsets for Efficient Verification2016

    • 著者名/発表者名
      Masaya Shimakawa, Yuuji Iwasaki, Shigeki Hagihara, Naoki Yonezaki
    • 学会等名
      Workshop on Computation: Theory and Practice (WCTP2016)
    • 発表場所
      フィリピン
    • 年月日
      2016-09-21 – 2016-09-22
    • 国際学会
  • [学会発表] Simple synthesis of reactive systems with tolerance for unexpected environmental behavior2016

    • 著者名/発表者名
      Shigeki Hagihara, Atsushi Ueno, Takashi Tomita, Masaya Shimakawa, Naoki Yonezaki
    • 学会等名
      Formal Methods in Software Engineering (FormaliSE '16)
    • 発表場所
      アメリカ
    • 年月日
      2016-05-15 – 2016-05-15
    • 国際学会

URL: 

公開日: 2018-01-16  

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

Powered by NII kakenhi