研究課題
本年度は無限小プログラミングを用いたハイブリッドシステム解析について,静的検証の重要な要素技術であるループ不変条件生成の研究を行った.具体的には,プログラムにおける遷移がプログラム変数の多項式で表現されるときに,同じくプログラム変数の多項式で表現される不変条件を生成する手法を研究した.最近研究が進んでいる IC3, ICE などの対話証明に基づく手法をベースに研究をすすめ,これらを代表者の専門である型システムを用いたプログラム検証の技術と融合させることにより,実用的な不変条件生成器を得ることができている.また,確率的動作を行うハイブリッドシステムのモデル化のための計算体系の研究も行った.具体的には,ハイブリッドシステムを設計する際にデファクトスタンダードとなっているデータフロー言語と呼ばれる種類の言語を確率的動作で拡張する研究をおこなった.現状では形式的な意味論を定義し,ランダムウォーク等の基本的な確率的動作が正しく表現できていることを確認した段階であるが,今後この言語の静的検証手法や無限小値での拡張を行うことによりハイブリッドシステムの研究につなげていく予定である.さらに,ハイブリッドシステムの重要な一要素であるソフトウェアについても検証手法の研究を行った.現在ハイブリッドシステムのためのソフトウェアは C 言語で記述されることが多い.しかし,C 言語は動的メモリ割り当てなどの低レベルの処理をプログラマが逐一記述しなければならないため,これらに起因するバグの混入が問題となる.本年度の研究は,C 言語におけるメモリリーク検証手法について,メモリ解放プリミティブが欠けている場合に自動的にこれらを挿入するためのプログラム変換の研究と,プログラムが無限ループに陥ったとしても一定の大きさのメモリ領域のみを消費することを保証する静的検証手法の研究をおこない発表した.
2: おおむね順調に進展している
ループ不変条件の生成というプログラム検証に欠くべからざる技術について重要な進展が得られていることは,本課題の進捗に大きな進展である.また,確率的動作は巨大なハイブリッドシステムのモデルを扱う際には特に重要となる.産業界のデファクトスタンダードであるデータフロー言語を確率的動作で拡張する研究は,未だ発展途上であるものの,本課題の成果の有用性に大きな意味を持つ.さらに,ソフトウェア検証手法においても前進が見られている.
本年度進展があったループ不変条件の生成手法については,知財化も検討した上で早めに発表し,さらに発展させる予定である.また,確率的データフロー言語については,無限小値との組み合わせを研究した上で,静的検証手法を研究することを考えている.C 言語のための静的検証手法については,実用に耐えうる検証ソフトウェアの実装を進めている.
すべて 2015 2014
すべて 雑誌論文 (3件) (うち査読あり 3件、 オープンアクセス 1件、 謝辞記載あり 3件) 学会発表 (4件)
EPTCS Proceedings 4th Workshop on Hybrid Autonomous Systems
巻: 174 ページ: 22--39
10.4204/EPTCS.174.3
Programming Languages and Systems - 12th Asian Symposium, {APLAS} 2014, Singapore, November 17-19, 2014, Proceedings
巻: 8858 ページ: 58--77
10.1007/978-3-319-12736-1_4
計測と制御
巻: 53 ページ: 1080--1085