2015 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 | サイバーフィジカルシステム / 入力生成問題 / 時相論理 / ロバスト意味論 |
|---|
| Outline of Annual Research Achievements |
本研究では、サイバーフィジカルシステム(CPS)のモデルベース開発において形式的手法を活用し、”correct by constructionなものづくり”の実現を目指す。特に、技術的には、これらシステムの設計開発の現場で必要不可欠となる入力生成問題に注力する。入力生成問題とは、与えられたシステムＳとシステムに対する仕様Ｐに対し、システムＳへの入力iであって、システム全体の動作Ｓ(i)が仕様Ｐを満たすようなものを求める問題である。ここでシステムＳはSimulinkのようなモデリング言語で、仕様Ｐは時相論理式として記述されるものとする。CPSの設計開発の現場において入力生成問題は、例えばエラー検出(仕様Ｐとして望ましくないエラーを取ることで、エラーが発生するシステムＳへの入力iを検出する)等、様々な応用における基礎的な問題として、極めて重要である。
この入力生成問題に対し、下記の2つの相補的なアプローチを統合することで、現場で運用可能なソルバを開発することが、本研究の最終目的である。1つのアプローチは、ロバスト意味論を用いた連続量最適化問題への帰着である。Breach [Donze et al., CAV ‘10]、S-TaLiRo [Annapureddy et al., TACAS `11]等のツールがこのアプローチに基づいて開発されている。もうひとつのアプローチとして、[赤崎 et al., HAS ‘14]で提案した、Hoare論理の事前条件および事後条件の計算による入力の演繹的導出が挙げられる。前者はシステムのダイナミクスが連続的な場合、後者は離散的な場合に特によい性質を持ち、両手法を統合することによって、大幅なスケーラビリティの向上が期待できる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
両手法を統合した入力生成問題のための枠組みを模索していくため、今年度は特にロバスト意味論を用いたアプローチについて、実際のCPS設計開発の現場で適用する場合の課題を調査することに力を置いた。
従来のロバスト意味論、特にSpace Robustness [Fainekos & Pappas, TCS ‘09] を用いたアプローチに基づくソルバでは、システムが離散的なダイナミクスに従う場合、帰着した連続量最適化問題がプラトー型の関数に対する最適化問題となってしまうため、入力生成が出来ない場合があるという問題があった。我々の今年度の成果の一つは、この問題を解決するため、先のSpace Robustness とTime Robustness [Donze & Maler, Formats ‘10] の両方のエッセンスを持つ新しい論理 Averaged STL およびその意味論を定義し、これに基づく入力生成問題ソルバをS-TaLiRoの実装に組み込んで、性能の向上を確認したことである [赤崎 & 蓮尾, CAV ‘15]。
また上記の成果および実際の設計開発現場での運用に堪えるツールの開発にむけたディスカッションのため、S-TaLiRoの開発グループであるアリゾナ州立大学のFainekosらの研究室、並びにBreachの開発等に協力しているカリフォルニア州のToyota Motor Engineering & Manufacturing North America, Inc. の研究所を訪問した。ここでAveraged STLのBreachへの共同実装も行われた。また既存のソルバで解けない入力生成問題のモデルケースについても情報交換を行った。
|
| Strategy for Future Research Activity |
今年度の研究においてロバスト意味論を用いたアプローチの現状を調査する中で、現段階で未解決なモデルケースの一部については、事前条件および事後条件の計算をサブシステムに対して繰り返し解くことによって、スケーラビリティが向上するという予測を立てた。これに基づき今年度は、連続量最適化問題への帰着および事前条件・事後条件の計算による演繹的導出という両手法の統合による問題の解決を目指す。
技術的課題として、一般にシステムの挙動が複雑である場合、事前条件・事後条件の計算が難しい場合があることが挙げられる。ここで我々は、現在連続量最適化問題のソルバとして盛んに研究されている、Gaussian Process Learning などの新しいアルゴリズムに注目している。これらアルゴリズムの特徴は、最適値を求める元の関数に対する予測を行いながら、その予測に基づいて最適化を行うことが挙げられる。今年度の主な目標は、この”予測”を事前条件・事後条件の近似として用いることで、Hoare論理のように入力の演繹的導出が可能であるか、調査を行うことである。
|
Research Products
(2 results)
