Realizability Decision and Program Synthesis for Reactive System Specification described by Temporal Logic

• Project/Area Number: 25330008
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: Saitama University
• Principal Investigator: YOSHIURA Noriaki 埼玉大学, 情報メディア基盤センター, 准教授 (00302969)
• Project Period (FY): 2013-04-01 – 2017-03-31
• Project Status: Completed (Fiscal Year 2016)
• Budget Amount: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000); Fiscal Year 2015: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2014: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000); Fiscal Year 2013: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
• Keywords: 時間論理 / モデルチェッキング / 実現可能性 / リアクティブシステム / 適切さの論理 / 仕様記述 / プログラム化可能性 / 仕様検証

Outline of Final Research Achievements

The research proposed the decision method that determinizes the realizabilities of reactive system specifications that are described in temporal logic. The method consists of the inference rules and the automata and can determine the unrealizibilties of the specifications fast. The research proposed the method of deducing constraint formulas of requirement for unrealizable reactive system specifications. The contraint formulas are useful to revise unrealizable reactive system specifications so that they may be realizable. The research also improves the inference system of relevant logic. The inference rule can deduce information from reactive system specifications. The information is useful so that the descriptors of the specifications can verify that the specifications are equal to what the specifications should be.
Moreover, the research proposed the verification method of OpenFlow software. The method can be a base of synthesizing OpenFlow software from network topologies.

Research Products

• [Journal Article] The Relation Between Syntax Restriction of Temporal Logic and Properties of Reactive System Specification (2017)
  • Author(s): Noriaki Yoshiura
  • Journal Title: Lecture Notes in Computer Science Volume: 10192 Pages: 105-114
  • Peer Reviewed
• [Journal Article] Computational Verification of Network Programs for Several OpenFlow Switches in Coq (2016)
  • Author(s): Hiroaki Date, Noriaki Yoshiura
  • Journal Title: Lecture Notes in Computer Science Volume: 9787 Pages: 223-238
  • Peer Reviewed
• [Journal Article] Shopping street safety using all-in-one-type security cameras (2014)
  • Author(s): K. Muramatsu, M. Ishizawa, A. Takita, N. Yoshiura, N. Ohta, K. Maru, H. Ueda and Y. Fujii,
  • Journal Title: ICIC Express Letters Volume: 8 Pages: 3001-3006
  • Peer Reviewed
• [Presentation] Computational Verification of Network Programs for serveral OpenFlow switches in Coq (2016)
  • Author(s): Hiroaki Date and Noriaki Yoshiura
  • Organizer: The 16th International Conference on Computational Science and Its Applications
  • Place of Presentation: 中国
  • Year and Date: 2016-07-04
  • Int'l Joint Research
• [Presentation] NetCoreプログラムのCoqによる検証 (2016)
  • Author(s): 伊達 弘明，吉浦 紀晃
  • Organizer: 情報処理学会第32回IOT研究会
  • Place of Presentation: 佐賀県
  • Year and Date: 2016-03-03
• [Presentation] Extracting Environmental Constraints in Reactive System Specifications (2015)
  • Author(s): Yuichi Fukaya and Noriaki Yoshiura
  • Organizer: 15th International Conference on Computational Science and Its Applications
  • Place of Presentation: カナダ
  • Year and Date: 2015-06-22
  • Int'l Joint Research
• [Presentation] Implementation of Decision Procedure of Stepwise Satisfiability of Reactive System Specifications (2015)
  • Author(s): Noriaki Yoshiura and Yuma Hirayanagi
  • Organizer: 15th International Conference on Computational Science and Its Applications
  • Place of Presentation: カナダ
  • Year and Date: 2015-06-22
  • Int'l Joint Research
• [Presentation] Implementation of Theorem Prover of Relevant Logic (2015)
  • Author(s): Noriaki Yoshiura
  • Organizer: 28th International Conference on Industrial, Engineering and Other Applications of Applied Intelligent Systems
  • Place of Presentation: 韓国
  • Year and Date: 2015-06-10
  • Int'l Joint Research
• [Presentation] 分解証明法を利用したリアクティブシステム仕様の強充足可能性判定器の提案 (2015)
  • Author(s): 中村 風太，吉浦 紀晃
  • Organizer: 情報処理学会 第187回ソフトウェア工学研究会
  • Place of Presentation: 東京都・千代田区
  • Year and Date: 2015-03-12 – 2015-03-13
• [Presentation] リアクティブシステム仕様の外部環境制約式に関する研究 (2015)
  • Author(s): 深谷 悠一，吉浦 紀晃
  • Organizer: 情報処理学会 第187回ソフトウェア工学研究会
  • Place of Presentation: 東京都・千代田区
  • Year and Date: 2015-03-12 – 2015-03-13
• [Presentation] Static Data Race Detection for Java Programs with Dynamic Class Loading (2014)
  • Author(s): Noriaki Yoshiura and Wei Wei
  • Organizer: 7th International Conference on Internet and Distributed Computing Systems
  • Place of Presentation: イタリア
  • Year and Date: 2014-09-22 – 2014-09-24
• [Presentation] Verification of System Requirements (2014)
  • Author(s): Noriaki Yoshiura
  • Organizer: 4th International Mechanical Engineering Research Conference
  • Place of Presentation: Cebu City, Philippines
• [Presentation] Construction and Verificationof Mobile Ad Hoc Network Protocols, In Proceedings of 5th International Symposium on Cyberspace Safety and Security, Lecture Notes in Computer Science, (2013)
  • Author(s): Natsuki Kimura and Noriaki Yoshiura
  • Organizer: 5th International Symposium on Cyberspace Safety and Security
  • Place of Presentation: Zhangjiajie, China
• [Presentation] Smart Street Light System Looking Like Usual Street Lights Based On Sensor Networks (2013)
  • Author(s): Noriaki Yoshiura, Yusaku Fujii and Naoya Ohta
  • Organizer: 13th International Symposium on Communications and Information Technologies
  • Place of Presentation: Samui, Thailand