2014 Fiscal Year Research-status Report
無限小プログラミングによるハイブリッドシステムの形式検証手法
| Project/Area Number |
25730040
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | ハイブリッドシステム / 無限小プログラミング / 形式手法 / 形式検証 / プログラミング言語 / プログラミング言語理論 / プログラム意味論 / 超準解析 |
|---|
| Outline of Annual Research Achievements |
本年度は無限小プログラミングを用いたハイブリッドシステム解析について，静的検証の重要な要素技術であるループ不変条件生成の研究を行った．具体的には，プログラムにおける遷移がプログラム変数の多項式で表現されるときに，同じくプログラム変数の多項式で表現される不変条件を生成する手法を研究した．最近研究が進んでいる IC3, ICE などの対話証明に基づく手法をベースに研究をすすめ，これらを代表者の専門である型システムを用いたプログラム検証の技術と融合させることにより，実用的な不変条件生成器を得ることができている．
また，確率的動作を行うハイブリッドシステムのモデル化のための計算体系の研究も行った．具体的には，ハイブリッドシステムを設計する際にデファクトスタンダードとなっているデータフロー言語と呼ばれる種類の言語を確率的動作で拡張する研究をおこなった．現状では形式的な意味論を定義し，ランダムウォーク等の基本的な確率的動作が正しく表現できていることを確認した段階であるが，今後この言語の静的検証手法や無限小値での拡張を行うことによりハイブリッドシステムの研究につなげていく予定である．
さらに，ハイブリッドシステムの重要な一要素であるソフトウェアについても検証手法の研究を行った．現在ハイブリッドシステムのためのソフトウェアは C 言語で記述されることが多い．しかし，C 言語は動的メモリ割り当てなどの低レベルの処理をプログラマが逐一記述しなければならないため，これらに起因するバグの混入が問題となる．本年度の研究は，C 言語におけるメモリリーク検証手法について，メモリ解放プリミティブが欠けている場合に自動的にこれらを挿入するためのプログラム変換の研究と，プログラムが無限ループに陥ったとしても一定の大きさのメモリ領域のみを消費することを保証する静的検証手法の研究をおこない発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
ループ不変条件の生成というプログラム検証に欠くべからざる技術について重要な進展が得られていることは，本課題の進捗に大きな進展である．また，確率的動作は巨大なハイブリッドシステムのモデルを扱う際には特に重要となる．産業界のデファクトスタンダードであるデータフロー言語を確率的動作で拡張する研究は，未だ発展途上であるものの，本課題の成果の有用性に大きな意味を持つ．さらに，ソフトウェア検証手法においても前進が見られている．
|
| Strategy for Future Research Activity |
本年度進展があったループ不変条件の生成手法については，知財化も検討した上で早めに発表し，さらに発展させる予定である．また，確率的データフロー言語については，無限小値との組み合わせを研究した上で，静的検証手法を研究することを考えている．C 言語のための静的検証手法については，実用に耐えうる検証ソフトウェアの実装を進めている．
|
Research Products
(7 results)
-
-
-
-
-
-
[Presentation] 京都大学 Teen Racketeer 養成コース2015
Author(s)
五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平
Organizer
第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015）
Place of Presentation
愛媛県松山市道後プリンスホテル
Year and Date
2015-03-04 – 2015-03-06
-
