| 研究実績の概要 |
本研究では、サイバーフィジカルシステム(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つのアプローチは手法が有効な問題が相補的な関係にあり、これらの理論的統合が実世界の入力生成問題に対して有効なソルバを導くと期待している。
|
| 今後の研究の推進方策 |
まず今年度5月を目途に、先で述べたアイデアに基づいた、元の仕様と因果関係をもつ他の条件も考慮した効率のよい入力生成アルゴリズムについての結果をまとめ、論文として投稿することを目指す。
さらに、上記の提案手法で仕様同士の因果関係を表すベイジアンネットワークについて、現在はユーザーが与えるという形式を取っているが、これを自動で生成することを目指す。技術的課題は、元の仕様Pと因果関係を持つ条件P_1,…,P_nをどのように導出するかであるが、現段階でPの事前・事後条件が条件P_1,…,P_nとしても有用となる場合があることが進行中の実験の知見として得られている。近年確率的プログラミングに関する事前・事後条件を計算に関しては盛んに研究が行われており[Olmedo et al., LICS 2016]、これによってベイジアンネットワークの構成に必要な条件P_1,…,P_nおよびそれらの間の条件つき確率を導出する。事前・事後条件を用いた入力生成のためのベイジアンネットワークの自動構成は、今年度10月に成果をまとめ論文として投稿することを目指す。
最終的にはこれらの研究を統合して得られた入力生成アルゴリズムを、成果として博士論文にまとめる。
|
