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

形式手法による定量的制約を満たす組み込みシステムの自動合成

研究課題

研究課題/領域番号 16K00092
研究種目

基盤研究(C)

配分区分基金
応募区分一般
研究分野 ソフトウェア
研究機関公立千歳科学技術大学 (2019-2021)
東北公益文科大学 (2017-2018)
東京工業大学 (2016)

研究代表者

萩原 茂樹  公立千歳科学技術大学, 理工学部, 准教授 (70334547)

研究期間 (年度) 2016-04-01 – 2022-03-31
研究課題ステータス 完了 (2021年度)
配分額 *注記
4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2019年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2018年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2017年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2016年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
キーワード形式手法 / 組み込みシステム / 自動合成 / 時間論理 / 検証 / 定量的制約 / 組込みシステム / システム検証・合成 / ソフトウェア工学 / 高信頼ソフトウェア開発
研究成果の概要

組み込みシステムは、機能要件などの定性的制約だけでなく、性能要件などの定量的制約を満たすことが強く望まれ、これら制約を必ず満たすシステムを構成する手法が必要不可欠である。厳密な保証が可能な形式手法により、これらの制約を満たす現実的なシステムを合成するための基礎技術を構成した。具体的には、性能要件をできるだけ満たすシステムの合成手法や、現実規模のシステム構成のためのモジュール分割方法などを構成した。

研究成果の学術的意義や社会的意義

現実的な仕様からシステムを系統的に構成する手法の研究は、ソフトウェア工学の分野で盛んに行われてきたが、それらはデータオリエンテッドな対応であり、それらから得られるのは「経験則」であると指摘されてきた。「法則」を得る方法として形式手法が注目されている。これまで形式手法は、解析に要する計算量の膨大さにより、現実規模の仕様に適用するのが困難であった。本研究は現実規模の仕様に対して、形式手法で解析が可能な範囲、即ち「法則」が適用可能な範囲を明確にするという学術的な特色がある。

報告書

(7件)
  • 2021 実績報告書   研究成果報告書 ( PDF )
  • 2020 実施状況報告書
  • 2019 実施状況報告書
  • 2018 実施状況報告書
  • 2017 実施状況報告書
  • 2016 実施状況報告書
  • 研究成果

    (19件)

すべて 2021 2020 2019 2018 2017 2016

すべて 雑誌論文 (12件) (うち査読あり 12件、 オープンアクセス 3件) 学会発表 (7件) (うち国際学会 6件)

  • [雑誌論文] Efficient Realizability Checking by Modularization of LTL Specifications2021

    • 著者名/発表者名
      Ito Sohei, Osari Kenji, Shimakawa Masaya, Hagihara Shigeki, Yonezaki Naoki
    • 雑誌名

      The Computer Journal

      巻: bxab116

    • DOI

      10.1093/comjnl/bxab116

    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] 地方公共サービスにおける人員・車両・施設等の最適資源配置問題 ―救急・消防に関する検討―2021

    • 著者名/発表者名
      三木潤一、川崎雄二郎、萩原茂樹
    • 雑誌名

      CIPFA Japan ジャーナル

      巻: 5 ページ: 25-35

    • NAID

      40022661491

    • 関連する報告書
      2020 実施状況報告書
    • 査読あり
  • [雑誌論文] Towards Interpretation of Abstract Instructions Using Declarative Constraints in Temporal Logic2020

    • 著者名/発表者名
      Masaya Shimakawa, Kentaro Hayashi, Shigeki Hagihara and Naoki Yonezaki
    • 雑誌名

      Proceedings of the 2020 9th International Conference on Software and Computer Applications (ICSCA2020)

      ページ: 17-20

    • DOI

      10.1145/3384544.3384572

    • 関連する報告書
      2019 実施状況報告書
    • 査読あり
  • [雑誌論文] Verification of Verifiability of Voting Protocols by Strand Space Analysis2019

    • 著者名/発表者名
      Shigeki Hagihara, Masaya Shimakawa and Naoki Yonezaki
    • 雑誌名

      Proceedings of the 2019 8th International Conference on Software and Computer Applications (ICSCA2019)

      ページ: 363-368

    • DOI

      10.1145/3316615.3316629

    • 関連する報告書
      2018 実施状況報告書
    • 査読あり
  • [雑誌論文] Towards Efficient Implementation of Realizability Checking for Reactive System Specifications2019

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

      Proceedings of the 2019 8th International Conference on Software and Computer Applications (ICSCA2019)

      ページ: 347-352

    • DOI

      10.1145/3316615.3316634

    • 関連する報告書
      2018 実施状況報告書
    • 査読あり
  • [雑誌論文] Compositional Analysis of Homeostasis of Gene Networks by Clustering Algorithms2018

    • 著者名/発表者名
      Sohei Ito, Kenji Osari, Shigeki Hagihara and Naoki Yonezaki
    • 雑誌名

      Biomedical Engineering Systems and Technologies (BIOSTEC 2017), Communications in Computer and Information Science

      巻: 881 ページ: 191-211

    • DOI

      10.1007/978-3-319-94806-5_11

    • ISBN
      9783319948058, 9783319948065
    • 関連する報告書
      2018 実施状況報告書
    • 査読あり
  • [雑誌論文] Efficiency of the strong satisfiability checking procedure for reactive system specifications2018

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

      AIP Conference Proceedings

      巻: 1955 ページ: 040051-040051

    • DOI

      10.1063/1.5033715

    • 関連する報告書
      2017 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Web server access trend analysis based on the Poisson distribution2017

    • 著者名/発表者名
      Shigeki Hagihara, Yoshiharu Fushihara, Masaya Shimakawa, Masahiko Tomoishi, Naoki Yonezaki
    • 雑誌名

      Proceedings of the 6th International Conference on Software and Computer Applications (ICSCA 2017)

      巻: - ページ: 256-261

    • DOI

      10.1145/3056662.3056701

    • 関連する報告書
      2017 実施状況報告書
    • 査読あり
  • [雑誌論文] Modularization of formal specifications for efficient synthesis of reactive systems2017

    • 著者名/発表者名
      Masaya Shimakawa, Kenji Osari, Shigeki Hagihara, Naoki Yonezaki
    • 雑誌名

      Proceedings of the 6th International Conference on Software and Computer Applications (ICSCA 2017)

      巻: - ページ: 208-213

    • DOI

      10.1145/3056662.3056702

    • 関連する報告書
      2017 実施状況報告書
    • 査読あり
  • [雑誌論文] Combining Unification and Rewriting in Proofs for Modal Logics with First-order Undefinable Frames2017

    • 著者名/発表者名
      Shigeki Hagihara, Masahiko Tomoishi, Masaya Shimakawa, Naoki Yonezaki
    • 雑誌名

      Advances in Engineering

      巻: 126 ページ: 676-683

    • DOI

      10.2991/icmmct-17.2017.140

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Safraless LTL Synthesis Considering Maximal Realizability2016

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

      Acta Informatica

      巻: Special Issue on Synthesis 号: 7 ページ: 1-38

    • DOI

      10.1007/s00236-016-0280-3

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Simple synthesis of reactive systems with tolerance for unexpected environmental behavior2016

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

      Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE '16)

      巻: - ページ: 15-21

    • DOI

      10.1145/2897667.2897672

    • 関連する報告書
      2016 実施状況報告書
    • 査読あり
  • [学会発表] 動的モデルによる救急隊配置の最適化手法―山形県酒田地区におけるケーススタディ2021

    • 著者名/発表者名
      川崎雄二郎, 萩原茂樹, 三木潤一
    • 学会等名
      日本応用数理学会第17回研究部会連合発表会
    • 関連する報告書
      2020 実施状況報告書
  • [学会発表] Towards Improvement of Realizability Checking for Reactive System Specifications by Simplification of Infinite Games2018

    • 著者名/発表者名
      Masaya Shimakawa, Shigeki Hagihara and Naoki Yonezaki
    • 学会等名
      Workshop on Computation: Theory and Practice (WCTP2018)
    • 関連する報告書
      2018 実施状況報告書
    • 国際学会
  • [学会発表] A Characterization on Necessary Conditions of Realizability for Reactive System Specifications2018

    • 著者名/発表者名
      Takashi Tomita, Masaya Shimakawa, Shigeki Hagihara and Naoki Yonezaki
    • 学会等名
      Workshop on Computation: Theory and Practice (WCTP2018)
    • 関連する報告書
      2018 実施状況報告書
    • 国際学会
  • [学会発表] Discussion on Verification of Voting Protocols2017

    • 著者名/発表者名
      Shigeki Hagihara, Masaya Shimakawa, Naoki Yonezaki
    • 学会等名
      17th Philippine Computing Science Congress (PCSC 2017)
    • 発表場所
      Cebu, Philippines
    • 年月日
      2017-03-16
    • 関連する報告書
      2016 実施状況報告書
    • 国際学会
  • [学会発表] Towards Improvements of Bounded Realizability Checking2017

    • 著者名/発表者名
      Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki
    • 学会等名
      Workshop on Computation: Theory and Practice (WCTP2017)
    • 関連する報告書
      2017 実施状況報告書
    • 国際学会
  • [学会発表] To develop software without flaws2016

    • 著者名/発表者名
      Shigeki Hagihara
    • 学会等名
      Workshop on Computation: Theory and Practice (WCTP2016), Satellite Conference
    • 発表場所
      Bohol, Philippines
    • 年月日
      2016-09-24
    • 関連する報告書
      2016 実施状況報告書
    • 国際学会
  • [学会発表] Discussion of LTL Subsets for Efficient Verification2016

    • 著者名/発表者名
      Masaya Shimakawa, Yuji Iwasaki, Shigeki Hagihara and Naoki Yonezaki
    • 学会等名
      Workshop on Computation: Theory and Practice (WCTP2016)
    • 発表場所
      Cebu, Philippines
    • 年月日
      2016-09-21
    • 関連する報告書
      2016 実施状況報告書
    • 国際学会

URL: 

公開日: 2016-04-21   更新日: 2023-01-30  

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

Powered by NII kakenhi