Synthesis of embedded systems satisfying quantitative constraints by formal methods

• Project/Area Number: 16K00092
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Chitose Institute of Science and Technology (2019-2021); Tohoku University of Community Service and Science (2017-2018); Tokyo Institute of Technology (2016)
• Principal Investigator: Hagihara Shigeki 公立千歳科学技術大学, 理工学部, 准教授 (70334547)
• Project Period (FY): 2016-04-01 – 2022-03-31
• Project Status: Completed (Fiscal Year 2021)
• Budget Amount: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000); Fiscal Year 2019: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2018: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000); Fiscal Year 2017: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2016: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
• Keywords: 形式手法 / 組み込みシステム / 自動合成 / 時間論理 / 検証 / 定量的制約 / 組込みシステム / システム検証・合成 / ソフトウェア工学 / 高信頼ソフトウェア開発

Outline of Final Research Achievements

Embedded systems are desired to satisfy not only qualitative constraints, but also quantitative constraints. Methods are required to develop systems which necessarily satisfy these constraints. We construct several fundamental techniques for synthesis of embedded systems of practical size, which satisfy these constraints by formal methods.

Academic Significance and Societal Importance of the Research Achievements

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

Research Products

• [Journal Article] Efficient Realizability Checking by Modularization of LTL Specifications (2021)
  • Author(s): Ito Sohei, Osari Kenji, Shimakawa Masaya, Hagihara Shigeki, Yonezaki Naoki
  • Journal Title: The Computer Journal Volume: bxab116
  • DOI: 10.1093/comjnl/bxab116
  • Peer Reviewed
• [Journal Article] 地方公共サービスにおける人員・車両・施設等の最適資源配置問題 ―救急・消防に関する検討― (2021)
  • Author(s): 三木潤一、川崎雄二郎、萩原茂樹
  • Journal Title: CIPFA Japan ジャーナル Volume: 5 Pages: 25-35
  • NAID: 40022661491
  • Peer Reviewed
• [Journal Article] Towards Interpretation of Abstract Instructions Using Declarative Constraints in Temporal Logic (2020)
  • Author(s): Masaya Shimakawa, Kentaro Hayashi, Shigeki Hagihara and Naoki Yonezaki
  • Journal Title: Proceedings of the 2020 9th International Conference on Software and Computer Applications (ICSCA2020) Pages: 17-20
  • DOI: 10.1145/3384544.3384572
  • Peer Reviewed
• [Journal Article] Verification of Verifiability of Voting Protocols by Strand Space Analysis (2019)
  • Author(s): Shigeki Hagihara, Masaya Shimakawa and Naoki Yonezaki
  • Journal Title: Proceedings of the 2019 8th International Conference on Software and Computer Applications (ICSCA2019) Pages: 363-368
  • DOI: 10.1145/3316615.3316629
  • Peer Reviewed
• [Journal Article] Towards Efficient Implementation of Realizability Checking for Reactive System Specifications (2019)
  • Author(s): Masaya Shimakawa, Atsushi Ueno, Shohei Mochizuki, Takashi Tomita, Shigeki Hagihara and Naoki Yonezaki
  • Journal Title: Proceedings of the 2019 8th International Conference on Software and Computer Applications (ICSCA2019) Pages: 347-352
  • DOI: 10.1145/3316615.3316634
  • Peer Reviewed
• [Journal Article] Compositional Analysis of Homeostasis of Gene Networks by Clustering Algorithms (2018)
  • Author(s): Sohei Ito, Kenji Osari, Shigeki Hagihara and Naoki Yonezaki
  • Journal Title: Biomedical Engineering Systems and Technologies (BIOSTEC 2017), Communications in Computer and Information Science Volume: 881 Pages: 191-211
  • DOI: 10.1007/978-3-319-94806-5_11
  • ISBN: 9783319948058, 9783319948065
  • Peer Reviewed
• [Journal Article] Efficiency of the strong satisfiability checking procedure for reactive system specifications (2018)
  • Author(s): Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki
  • Journal Title: AIP Conference Proceedings Volume: 1955 Pages: 040051-040051
  • DOI: 10.1063/1.5033715
  • Peer Reviewed / Open Access
• [Journal Article] Web server access trend analysis based on the Poisson distribution (2017)
  • Author(s): Shigeki Hagihara, Yoshiharu Fushihara, Masaya Shimakawa, Masahiko Tomoishi, Naoki Yonezaki
  • Journal Title: Proceedings of the 6th International Conference on Software and Computer Applications (ICSCA 2017) Volume: - Pages: 256-261
  • DOI: 10.1145/3056662.3056701
  • Peer Reviewed
• [Journal Article] Modularization of formal specifications for efficient synthesis of reactive systems (2017)
  • Author(s): Masaya Shimakawa, Kenji Osari, Shigeki Hagihara, Naoki Yonezaki
  • Journal Title: Proceedings of the 6th International Conference on Software and Computer Applications (ICSCA 2017) Volume: - Pages: 208-213
  • DOI: 10.1145/3056662.3056702
  • Peer Reviewed
• [Journal Article] Combining Unification and Rewriting in Proofs for Modal Logics with First-order Undefinable Frames (2017)
  • Author(s): Shigeki Hagihara, Masahiko Tomoishi, Masaya Shimakawa, Naoki Yonezaki
  • Journal Title: Advances in Engineering Volume: 126 Pages: 676-683
  • DOI: 10.2991/icmmct-17.2017.140
  • Peer Reviewed / Open Access
• [Journal Article] Safraless LTL Synthesis Considering Maximal Realizability (2016)
  • Author(s): Takashi Tomita, Atsushi Ueno, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki
  • Journal Title: Acta Informatica Volume: Special Issue on Synthesis Issue: 7 Pages: 1-38
  • DOI: 10.1007/s00236-016-0280-3
  • Peer Reviewed / Open Access
• [Journal Article] Simple synthesis of reactive systems with tolerance for unexpected environmental behavior (2016)
  • Author(s): Shigeki Hagihara, Atsushi Ueno, Takashi Tomita, Masaya Shimakawa, Naoki Yonezaki
  • Journal Title: Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE '16) Volume: - Pages: 15-21
  • DOI: 10.1145/2897667.2897672
  • Peer Reviewed
• [Presentation] 動的モデルによる救急隊配置の最適化手法―山形県酒田地区におけるケーススタディ (2021)
  • Author(s): 川崎雄二郎, 萩原茂樹, 三木潤一
  • Organizer: 日本応用数理学会第17回研究部会連合発表会
• [Presentation] Towards Improvement of Realizability Checking for Reactive System Specifications by Simplification of Infinite Games (2018)
  • Author(s): Masaya Shimakawa, Shigeki Hagihara and Naoki Yonezaki
  • Organizer: Workshop on Computation: Theory and Practice (WCTP2018)
  • Int'l Joint Research
• [Presentation] A Characterization on Necessary Conditions of Realizability for Reactive System Specifications (2018)
  • Author(s): Takashi Tomita, Masaya Shimakawa, Shigeki Hagihara and Naoki Yonezaki
  • Organizer: Workshop on Computation: Theory and Practice (WCTP2018)
  • Int'l Joint Research
• [Presentation] Discussion on Verification of Voting Protocols (2017)
  • Author(s): Shigeki Hagihara, Masaya Shimakawa, Naoki Yonezaki
  • Organizer: 17th Philippine Computing Science Congress (PCSC 2017)
  • Place of Presentation: Cebu, Philippines
  • Year and Date: 2017-03-16
  • Int'l Joint Research
• [Presentation] Towards Improvements of Bounded Realizability Checking (2017)
  • Author(s): Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki
  • Organizer: Workshop on Computation: Theory and Practice (WCTP2017)
  • Int'l Joint Research
• [Presentation] To develop software without flaws (2016)
  • Author(s): Shigeki Hagihara
  • Organizer: Workshop on Computation: Theory and Practice (WCTP2016), Satellite Conference
  • Place of Presentation: Bohol, Philippines
  • Year and Date: 2016-09-24
  • Int'l Joint Research
• [Presentation] Discussion of LTL Subsets for Efficient Verification (2016)
  • Author(s): Masaya Shimakawa, Yuji Iwasaki, Shigeki Hagihara and Naoki Yonezaki
  • Organizer: Workshop on Computation: Theory and Practice (WCTP2016)
  • Place of Presentation: Cebu, Philippines
  • Year and Date: 2016-09-21
  • Int'l Joint Research