| 研究課題/領域番号 |
24800035
|
|---|
| 研究種目 |
研究活動スタート支援
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
末永 幸平 京都大学, 学内共同利用施設等, 助教 (70633692)
|
|---|
| 研究期間 (年度) |
2012-08-31 – 2014-03-31
|
| 研究課題ステータス |
採択後辞退 (2013年度)
|
| 配分額 *注記 |
2,990千円 (直接経費: 2,300千円、間接経費: 690千円)
2013年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2012年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | ハイブリッドシステム / 超準解析 / 型システム / 静的検証 / 形式手法 / プログラミング言語 / ホーア論理 / 無限小プログラミング |
|---|
| 研究概要 |
前年度に提案した無限小プログラミングのための検証のフレームワークに基づいて無限小プログラムのホーア論理に基づく検証手法を提案し実装した．本実装は (1) バックエンドにおいて既存の自動定理証明器を拡張なしに用いることができるという点 (2) 既存研究でソフトウェアのための形式検証手法として提案された手法をそのまま用いることができる点に特徴がある．本研究は，ハイブリッドシステムの検証手法として無限小プログラミングの枠組みを利用するための重要なステップである．提案手法の理論的枠組と本実装に基づく実験結果を論文にまとめ，コンピュータを用いた検証に関する国際会議会議 (CAV) において発表した．
また，前年度まで手続き型言語として定式化されていた無限小プログラミングをストリーム処理言語に拡張した言語（超準ストリーム言語）の基礎づけと検証の研究を行った．ストリームは電気信号等により近い表現を持つため，本研究によってハイブリッドシステムの開発現場で用いられている設計図に直接形式検証を適用することが将来的に可能になると期待される．理論的にも (1) 超準化されたストリームと連続的な信号との関係 (2) 超準ストリームプログラムの不動点意味論 (3) 連続的信号を演繹的な検証手法である型システムで検証するための手法といった興味深い展開が見られている．本研究の内容を論文にまとめ，プログラミング言語の原理に関する国際会議 (POPL) において発表した．
|
| 現在までの達成度 (区分) |
理由
翌年度、交付申請を辞退するため、記入しない。
|
| 今後の研究の推進方策 |
翌年度、交付申請を辞退するため、記入しない。
|
