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

Extracting information for correction of flaws from embedded system specification of practical scale by formal method

Research Project

Project/Area Number 24500032
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Software
Research InstitutionTokyo Institute of Technology

Principal Investigator

HAGIHARA Shigeki  東京工業大学, 情報理工学(系)研究科, 助教 (70334547)

Research Collaborator SHIMAKAWA Masaya  東京工業大学, 大学院情報理工学研究科, 研究員 (00749161)
Project Period (FY) 2012-04-01 – 2015-03-31
Project Status Completed (Fiscal Year 2014)
Budget Amount *help
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2014: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2013: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
Fiscal Year 2012: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Keywords形式手法 / 組み込みシステム仕様 / 修正情報抽出 / 時間論理 / オートマトン / 極小充足不能集合 / 組込みシステム仕様
Outline of Final Research Achievements

For developing safety-critical embedded systems, verifying specification is expected to reduce the development costs of embedded systems. If a specification has flaws, we must correct the specification. It is desirable to obtain the cause and the location of flaws in the specifications. In this research, we proposed methods for obtaining the cause and the location and of flaws. In our methods, we manipulate omega-automata representing the specification to compute such information. We developed new reduction techniques for automata, and make such information computable for specifications of embedded systems at non-trivial scales. We proved correctness of our methods and clarified the time complexity of our methods. We also implemented our methods and got the tools.

Report

(4 results)
  • 2014 Annual Research Report   Final Research Report ( PDF )
  • 2013 Research-status Report
  • 2012 Research-status Report
  • Research Products

    (35 results)

All 2015 2014 2013 2012

All Journal Article (13 results) (of which Peer Reviewed: 10 results,  Open Access: 2 results) Presentation (21 results) Book (1 results)

  • [Journal Article] Verification and Optimization Methods for Mean-Payoff Temporal Logic2014

    • Author(s)
      冨田尭, 萩原茂樹, 米崎直樹
    • Journal Title

      Computer Software

      Volume: 31 Issue: 2 Pages: 2_93-2_117

    • DOI

      10.11309/jssst.31.2_93

    • NAID

      130004892285

    • ISSN
      0289-6540
    • Related Report
      2014 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Bounded Strong Satisfiability Checking of Reactive System Specifications2014

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

      IEICE Transactions on Information and Systems

      Volume: E97.D Issue: 7 Pages: 1746-1755

    • DOI

      10.1587/transinf.E97.D.1746

    • NAID

      130004519271

    • ISSN
      0916-8532, 1745-1361
    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Statistical Model Checking of Probabilistic Frequency Temporal Logic2014

    • Author(s)
      冨田尭, 萩原茂樹, 伊藤宗平, 米崎直樹
    • Journal Title

      Computer Software

      Volume: 31 Issue: 3 Pages: 3_336-3_356

    • DOI

      10.11309/jssst.31.3_336

    • NAID

      130004688291

    • ISSN
      0289-6540
    • Related Report
      2014 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Formal Analysis of Gene Networks using Network Motifs2014

    • Author(s)
      Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki
    • Journal Title

      Communications in Computer and Information Science

      Volume: 452 Pages: 131-146

    • DOI

      10.1007/978-3-662-44485-6_10

    • ISBN
      9783662444849, 9783662444856
    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] SAT solverを用いるLTLタブロー構成法とその評価2014

    • Author(s)
      安藤崇央, 萩原茂樹, 米崎直樹
    • Journal Title

      情報処理学会論文誌

      Volume: 55(2) Pages: 909-921

    • NAID

      110009665001

    • Related Report
      2013 Research-status Report
  • [Journal Article] A Formal Ontology of Interactions with Intensional Quantitative Semantics2013

    • Author(s)
      Takashi Tomita, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki
    • Journal Title

      Theory and Practice of Computation, Proceedings in Information and Communications Technology

      Volume: 7 Pages: 13-33

    • DOI

      10.1007/978-4-431-54436-4_2

    • ISBN
      9784431544357, 9784431544364
    • Related Report
      2013 Research-status Report
  • [Journal Article] Complexity of Strong Satisfiability Problems for Reactive System Specifications2013

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

      IEICE Transactions on Information and Systems

      Volume: E96-D(10) Pages: 2187-2193

    • NAID

      130004519200

    • Related Report
      2013 Research-status Report
  • [Journal Article] Developing Embedded Systems from Formal Specifications Written in Temporal Logic2013

    • Author(s)
      Shigeki Hagihara, Takahiro Arai, Masaya Shimakawa, Naoki Yonezaki
    • Journal Title

      Proceedings of the Third International Conference on Trends in Information, Telecommunication and Computing, Lecture Notes in Electrical Engineering

      Volume: 150 Pages: 107-113

    • DOI

      10.1007/978-1-4614-3363-7_13

    • ISBN
      9781461433620, 9781461433637
    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] Modular analysis of gene networks by linear temporal logic2013

    • Author(s)
      Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki
    • Journal Title

      Journal of Integrative Bioinformatics

      Volume: 10(2) Pages: 216-216

    • DOI

      10.2390/biecoll-jib-2013-216

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] SAT-Based Bounded Strong Satisfiability Checking of Reactive System Specifications2013

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

      Information and Communicatiaon Technology, Lecture Notes in Computer Science

      Volume: 7804 Pages: 60-70

    • DOI

      10.1007/978-3-642-36818-9_7

    • NAID

      40022046973

    • ISBN
      9783642368172, 9783642368189
    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] Completeness of a Deduction System for Relational Information between Ciphertexts based on Probabilistic Computational Semantics2012

    • Author(s)
      Shigeki Hagihara, Hiroaki Oguro, Naoki Yonezaki
    • Journal Title

      Theory and Practice of Computation, Proceedings in Information and Communications Technology

      Volume: 5 Pages: 116-132

    • DOI

      10.1007/978-4-431-54106-6_10

    • ISBN
      9784431541059, 9784431541066
    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] A Temporal Logic with Mean-Payoff Constraints2012

    • Author(s)
      Takashi Tomita, Shin Hiura, Shigeki Hagihara, Naoki Yonezaki
    • Journal Title

      Formal Methods and Software Engineering, Lecture Notes in Computer Science

      Volume: 7635 Pages: 249-265

    • DOI

      10.1007/978-3-642-34281-3_19

    • ISBN
      9783642342806, 9783642342813
    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] Kripke semantics for Epistemic Logic of Relational Information between Ciphertexts2012

    • Author(s)
      Shigeki Hagihara, Hiroaki Oguro, Naoki Yonezaki
    • Journal Title

      Philippine Computing Journal

      Volume: 7(2) Pages: 23-32

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Presentation] 環境許容性のあるリアクティブシステム合成法2015

    • Author(s)
      上野篤史, 冨田尭, 島川昌也, 萩原茂樹, 米崎直樹
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会
    • Place of Presentation
      沖縄県青年会館
    • Year and Date
      2015-03-09 – 2015-03-10
    • Related Report
      2014 Annual Research Report
  • [Presentation] A new approach to analysis of access tendency of web server using Poisson distribution2015

    • Author(s)
      Yoshiharu Fushihara, Shigeki Hagihara, Masahiko Tomoishi, Naoki Yonezaki
    • Organizer
      15th Philippine Computing Science Congress (PCSC2015)
    • Place of Presentation
      University of St. Louis, Philippines
    • Year and Date
      2015-03-05 – 2015-03-07
    • Related Report
      2014 Annual Research Report
  • [Presentation] Approximate Analysis of Homeostasis of Gene Networks by Linear Temporal Logic using Network Motifs2015

    • Author(s)
      Sohei Ito, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      6th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2015)
    • Place of Presentation
      Lisbon Marriott Hotel, Portugal
    • Year and Date
      2015-01-12 – 2015-01-15
    • Related Report
      2014 Annual Research Report
  • [Presentation] Discussion on modularization of specifications for efficient synthesis of reactive systems2014

    • Author(s)
      Kenji Osari, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      Symposium on the Mathematical Aspects of Computer Science 2014 (SMACS 2014)
    • Place of Presentation
      Ateneo de Naga University, Philippines
    • Year and Date
      2014-11-24 – 2014-11-28
    • Related Report
      2014 Annual Research Report
  • [Presentation] Fast Translation from LTL to Buechi Automata via Non-transition-based Automata2014

    • Author(s)
      Shohei Mochizuki, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      16th International Conference on Formal Engineering Methods, ICFEM 2014
    • Place of Presentation
      Melia Hotel, Luxembourg
    • Year and Date
      2014-11-03 – 2014-11-07
    • Related Report
      2014 Annual Research Report
  • [Presentation] An Efficient Implementation of Satisfiability Checking for LTL with Mean-Payoff Constraints2014

    • Author(s)
      Takashi Tomita, Takahito Kimura, Shigeki Hagihara and Naoki Yonezaki
    • Organizer
      Workshop on Computation: Theory and Practice (WCTP2014)
    • Place of Presentation
      フィリピン大学セブ校, センチュリーパークホテル(マニラ)
    • Year and Date
      2014-10-03 – 2014-10-07
    • Related Report
      2014 Annual Research Report
  • [Presentation] Minimal strongly unsatisfiable subsets of reactive system specifications2014

    • Author(s)
      Shigeki Hagihara, Naoki Egawa, Masaya Shimakawa, Naoki Yonezaki
    • Organizer
      the 29th ACM/IEEE international conference on Automated software engineering (ASE2014)
    • Place of Presentation
      Aros Congress Center, Vasteras, Sweden
    • Year and Date
      2014-09-15 – 2014-09-19
    • Related Report
      2014 Annual Research Report
  • [Presentation] 協調的リアクティブシステムの合成手法2014

    • Author(s)
      冨田尭, 上野篤史, 萩原茂樹, 米崎直樹
    • Organizer
      日本ソフトウェア科学会第31回大会
    • Place of Presentation
      名古屋大学
    • Year and Date
      2014-09-07 – 2014-09-10
    • Related Report
      2014 Annual Research Report
  • [Presentation] リアクティブシステム仕様の極小強充足不能部分計算に関する考察2014

    • Author(s)
      萩原茂樹, 江川直毅, 島川昌也, 米崎直樹
    • Organizer
      情報処理学会第99回プログラミング研究発表会
    • Place of Presentation
      旭川市民文化会館
    • Year and Date
      2014-06-19 – 2014-06-20
    • Related Report
      2014 Annual Research Report
  • [Presentation] A Qualitative Framework for Analysing homeostasis in Gene Networks2014

    • Author(s)
      Sohei Ito, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      5th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2014)
    • Place of Presentation
      Angers, France
    • Related Report
      2013 Research-status Report
  • [Presentation] On Constructing Unification-based Proof Methods for Modal Logics with First-order Undefinable Frames2014

    • Author(s)
      Shigeki Hagihara, Masahiko Tomoishi, Naoki Yonezaki
    • Organizer
      14th Philippine Computing Science Congress
    • Place of Presentation
      University of Immaculate Conception, Davao City, Philippines
    • Related Report
      2013 Research-status Report
  • [Presentation] 確率的環境下において平均利得時間論理仕様を実現する最適マルコフ決定過程の自動合成法2013

    • Author(s)
      冨田尭, 山崎徹郎, 萩原茂樹, 米崎直樹
    • Organizer
      日本ソフトウェア科学会第30回大会
    • Place of Presentation
      東京大学
    • Related Report
      2013 Research-status Report
  • [Presentation] LTL式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装に関する研究2013

    • Author(s)
      上野篤史, 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹
    • Organizer
      日本ソフトウェア科学会第30回大会
    • Place of Presentation
      東京大学
    • Related Report
      2013 Research-status Report
  • [Presentation] An object-oriented language for parameterised reactive system specification based on linear temporal logic2013

    • Author(s)
      Kenji Osari, Takuya Murooka, Kiyotaka Hagiwara, Takahiro Ando, Masaya Shimakawa, Sohei Ito, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      Workshop on Computation: Theory and Practice (WCTP2013)
    • Place of Presentation
      サンホセ-レコレトス大学, フィリピン大学
    • Related Report
      2013 Research-status Report
  • [Presentation] 強充足不能なリアクティブシステム仕様における欠陥範囲の特定2013

    • Author(s)
      萩原茂樹, 江川直毅, 島川昌也, 米崎直樹
    • Organizer
      日本ソフトウェア科学会 FOSE 2013
    • Place of Presentation
      加賀
    • Related Report
      2013 Research-status Report
  • [Presentation] Qualitative analysis of gene regulatory networks using network motifs2013

    • Author(s)
      Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      proceedings of 4th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2013)
    • Place of Presentation
      Barcelona, Spain
    • Related Report
      2012 Research-status Report
  • [Presentation] Mean-Payoff制約を記述可能な線形時間論理2012

    • Author(s)
      冨田尭, 萩原茂樹, 米崎直樹
    • Organizer
      日本ソフトウェア科学会第29回大会
    • Place of Presentation
      法政大学小金井キャンパス
    • Related Report
      2012 Research-status Report
  • [Presentation] Complexity of Checking Strong Satisfiability of Reactive System Specifications2012

    • Author(s)
      Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      International Conference on Advances in Information Technology and Communication, AIT 2012
    • Place of Presentation
      dubai, UAE
    • Related Report
      2012 Research-status Report
  • [Presentation] A Formal Ontology of Interactions with Intensional Quantitative Semantics2012

    • Author(s)
      Takashi Tomita, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      Workshop on Computation: Theory and Practice (WCTP-2012)
    • Place of Presentation
      Manila, Philippines
    • Related Report
      2012 Research-status Report
  • [Presentation] Modular analysis of gene networks using temporal logic (abstract)2012

    • Author(s)
      Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki
    • Organizer
      5th Annual RECOMB Conference on Regulatory and Systems Genomics, with DREAM Challenges
    • Place of Presentation
      San Francisco, USA
    • Related Report
      2012 Research-status Report
  • [Presentation] LTL式からBuchiオートマトンへの高速な変換法2012

    • Author(s)
      望月翔平, 島川昌也, 萩原茂樹, 米崎直樹
    • Organizer
      ソフトウェア工学の基礎XIX, 日本ソフトウェア科学会 FOSE2012
    • Place of Presentation
      由布院
    • Related Report
      2012 Research-status Report
  • [Book] 応用数理ハンドブック(論理的検証法の節、pp. 238-239)2013

    • Author(s)
      萩原茂樹(分担執筆)
    • Total Pages
      685
    • Publisher
      朝倉書店
    • Related Report
      2013 Research-status Report

URL: 

Published: 2013-05-31   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi