無限小プログラミングによるハイブリッドシステムの形式検証手法
| 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 *help |
¥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 |
翌年度、交付申請を辞退するため、記入しない。
|
Report
(1 results)
Research Products
(8 results)
