• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Cooperative Reactive System Synthesis Based on Necessary Conditions of Realizability

Research Project

Project/Area Number 17K17763
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeMulti-year Fund
Research Field Computer system
Software
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

Tomita Takashi  北陸先端科学技術大学院大学, 情報社会基盤研究センター, 講師 (80749226)

Project Period (FY) 2017-04-01 – 2023-03-31
Project Status Completed (Fiscal Year 2022)
Budget Amount *help
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2019: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2018: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Keywordsソフトウェア工学 / ソフトウェア検証 / 形式手法 / 協調的リアクティブシステム / 実現可能性 / 自動合成 / 協調的リテクティブシステム
Outline of Final Research Achievements

In this research, we tackled the development of an automatic synthesis method of a cooperative reactive system from a formal requirement specification, based on necessary conditions of realizability of the specification.
We found eight new necessary conditions of the realizability, gave a systematic characterization for the new conditions and also existing ones, and proof a hierarchy theorem among the conditions. The conditions are systematically categorized with four viewpoints: exhaustivity, strategizability, preservability and stability. In these viewpoints, we can analyze defects of specifications and also imply the possibility of cooperation between a reactive system and external environment. We also revealed expected complexities of checking problems for the necessary conditions, based on the similarity among subroutines of their checking procedures. That is, we established the basis of cooperative reactive system synthesis methods based on necessary conditions of realizability.

Academic Significance and Societal Importance of the Research Achievements

本研究成果は,より現実的・一般的な自動合成技術の基盤を与えたという点で学術的・社会的な意義がある.
古典的なリアクティブシステム自動合成では敵対的な環境を想定するという過度に厳しい安全性に基づいていたが,本研究では協調の発生を想定し緩和された安全性に基づく自動合成に注目し,合成可能性の基盤となる実現可能性必要条件群について分析した.その結果,実現可能性必要条件群の判定手続きの期待計算量は大きいものの,体系的な特徴付け・分類により,要求仕様の欠陥や協調不調についてのより詳細な分析が可能なことが明らかになったため,仕様修正の容易化を期待できる.

Report

(7 results)
  • 2022 Annual Research Report   Final Research Report ( PDF )
  • 2021 Research-status Report
  • 2020 Research-status Report
  • 2019 Research-status Report
  • 2018 Research-status Report
  • 2017 Research-status Report
  • Research Products

    (5 results)

All 2022 2020 2018

All Journal Article (2 results) (of which Peer Reviewed: 2 results,  Open Access: 2 results) Presentation (3 results) (of which Int'l Joint Research: 2 results)

  • [Journal Article] A Characterization on Necessary Conditions of Realizability for Reactive System Specifications2022

    • Author(s)
      TOMITA Takashi、HAGIHARA Shigeki、SHIMAKAWA Masaya、YONEZAKI Naoki
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: E105.D Issue: 10 Pages: 1665-1677

    • DOI

      10.1587/transinf.2021FOP0005

    • ISSN
      0916-8532, 1745-1361
    • Year and Date
      2022-10-01
    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] A Characterization on Necessary Conditions of Realizability for Reactive System Specifications2022

    • Author(s)
      Takashi Tomita, Shigeki Hagihara, Masaya Shimakawa, Naoki Yonezaki
    • Journal Title

      IEICE Transaction on Information and Systems

      Volume: E105-D

    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Open Access
  • [Presentation] リアクティブシステム実現可能性必要条件の判定手続き2020

    • Author(s)
      冨田 尭
    • Organizer
      日本ソフトウェア科学会第37回大会
    • Related Report
      2020 Research-status Report
  • [Presentation] A Characterization on Necessary Conditions of Realizability for Reactive System Specifications2018

    • Author(s)
      Takashi Tomita, Shigeki Hagihara, Masaya Shimakawa, Naoki Yonezaki
    • Organizer
      Workshop on Computation: Theory and Practice
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] Towards Efficient Implementation of Realizability Checking for Reactive System Specifications2018

    • Author(s)
      Masaya Shimakawa, Atsushi Ueno, Shohei Mochizuki, Takashi Tomita, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      8th International Conference on Software and Computer Applications
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research

URL: 

Published: 2017-04-28   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi