無限小プログラミングによるハイブリッドシステムの形式検証手法

• Project/Area Number: 24800035
• Research Category: Grant-in-Aid for Research Activity Start-up
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: Kyoto University
• Principal Investigator: 末永 幸平 京都大学, 学内共同利用施設等, 助教 (70633692)
• Project Period (FY): 2012-08-31 – 2014-03-31
• Project Status: Declined (Fiscal Year 2013)
• Budget Amount: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000); Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2012: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
• Keywords: ハイブリッドシステム / 超準解析 / 型システム / 静的検証 / 形式手法 / プログラミング言語 / ホーア論理 / 無限小プログラミング

Research Abstract

前年度に提案した無限小プログラミングのための検証のフレームワークに基づいて無限小プログラムのホーア論理に基づく検証手法を提案し実装した．本実装は (1) バックエンドにおいて既存の自動定理証明器を拡張なしに用いることができるという点 (2) 既存研究でソフトウェアのための形式検証手法として提案された手法をそのまま用いることができる点に特徴がある．本研究は，ハイブリッドシステムの検証手法として無限小プログラミングの枠組みを利用するための重要なステップである．提案手法の理論的枠組と本実装に基づく実験結果を論文にまとめ，コンピュータを用いた検証に関する国際会議会議 (CAV) において発表した．
また，前年度まで手続き型言語として定式化されていた無限小プログラミングをストリーム処理言語に拡張した言語（超準ストリーム言語）の基礎づけと検証の研究を行った．ストリームは電気信号等により近い表現を持つため，本研究によってハイブリッドシステムの開発現場で用いられている設計図に直接形式検証を適用することが将来的に可能になると期待される．理論的にも (1) 超準化されたストリームと連続的な信号との関係 (2) 超準ストリームプログラムの不動点意味論 (3) 連続的信号を演繹的な検証手法である型システムで検証するための手法といった興味深い展開が見られている．本研究の内容を論文にまとめ，プログラミング言語の原理に関する国際会議 (POPL) において発表した．

Current Status of Research Progress

Reason

翌年度、交付申請を辞退するため、記入しない。

Strategy for Future Research Activity

翌年度、交付申請を辞退するため、記入しない。

Research Products

• [Journal Article] Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals (2013)
  • Author(s): Kohei Suenaga, Hiroyoshi Sekine, and
  • Journal Title: Proc. POPL Volume: 40 Pages: 417-430
  • DOI: 10.1145/2429069.2429120
  • Peer Reviewed
• [Journal Article] Type-based Safe Resource Deallocation for Shared-Memory Concurrency (2012)
  • Author(s): Kohei Suenaga, Ryota Fukuda, Atsushi Igarashi
  • Journal Title: Proc. of ACM OOPSLA Volume: 27 Pages: 1-20
  • DOI: 10.1145/2384616.2384618
  • Peer Reviewed
• [Journal Article] Exercises in Nonstandard Static Analysis of Hybrid Systems (2012)
  • Author(s): Ichiro Hasuo and Kohei Suenaga
  • Journal Title: Proc. Computer Aided Verification - 24th International Conference, Lecture Notes in Computer Science Volume: 7358 Pages: 462-478
  • DOI: 10.1007/978-3-642-31424-7_34
  • ISBN: 9783642314230, 9783642314247
  • Peer Reviewed
• [Presentation] Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals (2013)
  • Author(s): Ichiro Hasuo
  • Organizer: ACM Conference of 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013)
  • Place of Presentation: Rome, Italy
• [Presentation] Hyperstream Processing Systems --- Nonstandard Modeling of Continuous-Time Signals (2013)
  • Author(s): 蓮尾 一郎
  • Organizer: PPL 2013 (プログラミングおよびプログラミング言語ワークショップ)
  • Place of Presentation: 福島県
• [Presentation] Type-Based Safe Resource Deallocation for Shared-Memory Concurrency (2013)
  • Author(s): 末永 幸平
  • Organizer: PPL 2013 (プログラミングおよびプログラミング言語ワークショップ)
  • Place of Presentation: 福島県
• [Presentation] Type-Based Safe Resource Deallocation for Shared-Memory Concurrency (2012)
  • Author(s): Ryota Fukuda
  • Organizer: The 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012
  • Place of Presentation: AZ, USA
• [Remarks] Kohei Suenaga
  • URL: http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/