2015 Fiscal Year Annual Research Report
| Project/Area Number |
15J05580
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
木戸 肩吾 東京大学, 情報理工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2015-04-24 – 2018-03-31
|
| Keywords | ハイブリッドシステム / サイバーフィジカルシステム / 形式検証 / 超準解析 |
|---|
| Outline of Annual Research Achievements |
自動車，飛行機といったシステムは制御プログラムの離散的な振る舞いと，物理環境下での微分方程式で表わされるような連続的な振る舞いとの双方を含んでいるという意味でハイブリッドシステムと呼ばれる．自動運転車などの開発が進められている現在，安全なハイブリッドシステムの開発は産業的にも非常に重要な課題である．私の研究は本来離散的なプログラムに対して適用する目的で研究されてきた形式検証手法を連続的な振る舞いに対しても適用できるよう超準解析により拡張し，ハイブリッドシステムの検証手法を提案し，これにより安全なハイブリッドシステム開発を支援する．
本年度はまず修士課程在学中より行ってきた抽象解釈という形式検証手法の超準解析による拡張に関わる研究を継続して行い，ハイブリッドシステムの解析に関する国際ワークショップSNR'15とモデル検査及び抽象解釈に関する国際学会VMCAI'16にて口頭発表を行った．
また，SNR'15に参加した際にフランス・Ecole Normale Superieureの抽象解釈に関する研究グループAntique Project Teamの筆頭研究者であるDr. Xavier Rivalとのコンタクトを得，2016年の1月末より約1ヶ月間パリで共同研究を行った．
他に，研究実施計画の通り，来年度以降のモデル検査という形式検証手法の超準解析による拡張に向けてサーベイを行った．自分の口頭発表を行ったSNR'15とVMCAI'16に加え，それぞれに併設されていたCAV'15及びPOPL'16，さらに京都で開催された国際学会ICALP'15及びLICS'15に参加し，分野の動向調査を行った．本年度のサーベイに基づき，来年度以降モデル検査の超準解析による拡張に取り組んでいく予定である．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
まず本年度の学術的な成果として，修士課程在学中より行ってきた抽象解釈という形式検証手法の超準解析による拡張に関わる研究を継続して行い，ハイブリッドシステムの解析に関する国際ワークショップSNR'15[Kido, Chaudhuri & Hasuo, SNR'15]とモデル検査及び抽象解釈に関する国際学会VMCAI'16[Kido, Chaudhuri & Hasuo, VMCAI'16]にそれぞれ採択され，自身が口頭発表を行った．
抽象解釈の拡張についてSNR’15で口頭発表を行った際，併設の国際学会CAV’15にて抽象解釈に関する研究発表[Oulamara & Venet, CAV’15]があり，その筆頭著者であるMendes Oulamaraの紹介によりフランス・Ecole Normale Superieureの抽象解釈に関する研究グループAntique project teamへの研究訪問を行うこととなった．この研究訪問中は抽象解釈の拡張によるハイブリッドシステム検証をより大規模で複雑なハイブリッドシステムに適用するための研究を行った．これは当初計画していなかったことであり，本研究は当初の計画以上の進展を見せていると言える理由の一つである．これらに関しては研究途中であり，2016年度も引き続き研究を行う．
他に，モデル検査という形式検証手法のサーベイも当初の計画通り行うことができ，来年度以降モデル検査の超準解析による拡張に取り組んでいくつもりである．
また，他に当初の計画以上に進展していることとして，来年度以降に向けたアプローチとしてカナダ・Waterloo大学でシステム工学を研究しているKrzysztof Czarnecki教授との議論を開始した．来年度中にWaterloo大学を訪問し共同研究を行う予定である．
|
| Strategy for Future Research Activity |
まず，本年度にフランス・Ecole Normale Superieureの抽象解釈に関する研究グループAntique project teamを研究訪問した際から進めている，抽象解釈を超準解析で拡張することによるハイブリッドシステム検証のさらなる拡張に向けた研究を引き続き進めていく．
また，本年度はモデル検査という形式検証手法の超準解析による拡張に向けてサーベイを計画通りに行うことができたため，これらのサーベイに基づき，来年度以降モデル検査の超準解析による拡張に取り組んでいく．
他に2016年度以降に向けたアプローチとして，カナダ・Waterloo大学でシステム工学の研究をしているKrzysztof Czarnecki教授との議論を開始している．私の専門とする形式検証手法をシステム工学の手法と組み合わせることで自動車などのハイブリッドシステムの開発支援を行うことを目的とした，より応用に近い研究を行いたいと考えており．来年度中にはWaterloo大学を訪問し，共同研究を行う予定である．
|
