2016 Fiscal Year Annual Research Report
形式的手法とサイバーフィジカルシステム設計開発との相互拡張
| Project/Area Number |
15J09877
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
赤崎 拓未 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2015-04-24 – 2018-03-31
|
| Keywords | 入力生成問題 / falsification / temporal logic / quantitative logic / Gaussian process |
|---|
| Outline of Annual Research Achievements |
本研究では、サイバーフィジカルシステム(CPS)のモデルベース開発において形式的手法を活用し、”correct by constructionなものづくりの実現”を目指す。特に、入力生成問題を解く効率的なアルゴリズムの開発を目指す。入力生成問題とは、与えられたシステムSとシステムに対する仕様Pに対し、システムの入力 iであって、システム全体の動作S(i)が仕様Pを満たすようなものを求める問題であり、システムのエラー検出(仕様Pとして望ましくないエラー状態を取ることで、システムがエラー状態に陥る入力iを検出する)や経路生成(この場合は仕様Pとしてシステムにたどり着いてほしい終状態をとる)等、様々な応用に対する一般的な定式化である。
本研究の最終目標は、下記の2つの相補的な既存のアプローチを統合し、実世界に現れる入力生成問題に適用可能なスケーラビリティを持つソルバを開発することである。1つは、ロバスト意味論を用いて連続量最適化問題へ帰着する、機械学習的なアプローチである。現在の主流はこちらであり、Breach [Donze et al., CAV 2010]やS-TaLiRo [Annapureddy et al., TACAS 2011] などのソルバがこれに基づいて開発されている。もう１つは、Hoare論理における事前事後条件の計算によって入力を演繹的に導出する計算論理学的なアプローチである。[赤崎 et al., HAS 2014]では、限られたクラスのCPSに対して、命令型言語で書かれたプログラムの場合と同様に仕様Pを満たすために入力iが満たすべき条件をシステムの構成から帰納的に計算する方法が提案された。これらの2つのアプローチは手法が有効な問題が相補的な関係にあり、これらの理論的統合が実世界の入力生成問題に対して有効なソルバを導くと期待している。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
今年度は、連続量最適化問題のソルバとして盛んに研究されている、ガウス過程最適化などのアルゴリズムに注目して研究を行った。これらアルゴリズムの特徴は、最適値を求める元の関数に対する予測を行いながら、その予測に基づいて最適化を行うことである。当初は、この予測を事前条件・事後条件の近似として用いることで、Hoare論理のように入力の演繹的導出を行うというアイデアで研究を進めた。
まず、入力生成問題の一ケースである条件付き安全性のエラー検出に絞って、この効率的な解法の開発に注力した。この問題の難しいところは、ランダムな入力のもとではシステムの動作が前提条件を満たすことが稀である場合、エラーが検出される可能性が極めて低くなってしまうことである。これは機械学習的アプローチに基づく現在の主流の入力生成問題ソルバ共通の弱点である。この問題に対し、前提条件が満たされる入力空間における領域をガウス過程を用いて予測することで、既存手法に比べ比較して高確率で前提条件を満たす入力を生成しながらエラー検出を行うアルゴリズムを提案した。この成果は国際会議RV2016において発表が行われた。
さらに、先の手法を条件付き安全性からより一般の場合に拡張することを試みた。条件付き安全性の効率的なエラー検出においては、元の条件付き安全性という仕様のほかに、その部分式にあたる前提条件についても注目することで、ソルバの性能向上を図った。これを一般化し、元々の仕様のロバストさだけでなく、それと因果関係を持つ他の条件にも注目して入力生成を行う。具体的には、条件同士の因果関係がベイジアンネットワークとして与えられた場合、入力生成問題を仕様Pのロバストさの最小化問題ではなく、仕様Pを仮定した条件付確率との確率分布の距離の最小化問題として帰着する。現在は上記のアイデアに基づいた実験および論文の執筆を進行中である。
|
| Strategy for Future Research Activity |
まず今年度5月を目途に、先で述べたアイデアに基づいた、元の仕様と因果関係をもつ他の条件も考慮した効率のよい入力生成アルゴリズムについての結果をまとめ、論文として投稿することを目指す。
さらに、上記の提案手法で仕様同士の因果関係を表すベイジアンネットワークについて、現在はユーザーが与えるという形式を取っているが、これを自動で生成することを目指す。技術的課題は、元の仕様Pと因果関係を持つ条件P_1,…,P_nをどのように導出するかであるが、現段階でPの事前・事後条件が条件P_1,…,P_nとしても有用となる場合があることが進行中の実験の知見として得られている。近年確率的プログラミングに関する事前・事後条件を計算に関しては盛んに研究が行われており[Olmedo et al., LICS 2016]、これによってベイジアンネットワークの構成に必要な条件P_1,…,P_nおよびそれらの間の条件つき確率を導出する。事前・事後条件を用いた入力生成のためのベイジアンネットワークの自動構成は、今年度10月に成果をまとめ論文として投稿することを目指す。
最終的にはこれらの研究を統合して得られた入力生成アルゴリズムを、成果として博士論文にまとめる。
|
Research Products
(2 results)
