| 研究課題/領域番号 |
15KT0012
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
蓮尾 一郎 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (60456762)
|
|---|
| 研究分担者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| 研究期間 (年度) |
2015-07-10 – 2020-03-31
|
| キーワード | 物理情報システム / 形式検証 / テスト / ハイブリッドシステム / 数理論理学 / 統計的機械学習 / 圏論 / プログラム理論 |
|---|
| 研究実績の概要 |
ソフトウェア科学における諸手法のシステム工学への応用という最終目標に対して，多様なトピックにおいて大きな進展があった．
まず，実システムに適用可能とするためのスケーラビリティの向上のため，確率的最適化をはじめとする統計的機械学習の活用に取り組んだ．具体的にはハイブリッドシステムの反例生成のための効率的アルゴリズムの研究に取り組み，既存の連続量最適化ベースの手法の実効性をモンテカルロ木探索により向上させた成果を，組込みシステム分野のトップ国際会議 EMSOFT'18 にて発表した．また，同種のアイデアを用いて，仕様における論理結合子の解釈という当該分野でよく知られた問題を解決した成果は，システム検証分野の旗艦国際会議 CAV'19に採択された．
昨年度から引き続き取り組んだ実行時モニタリングの研究においても，顕著な成果を上げた．具体的成果は以下の通り．1) ネットワークを介したモニタリングのための通信量圧縮のためのフィルタリング手法を考案し，EMSOFT'18（上述）に同じく採択された．この成果については特許出願中である．2) パリ13大学の研究者を長期滞在者として迎え，特にパラメータを許す仕様に対するモニタリング手法の研究が大きく進展した．この成果は，トップ国際会議 ICECCS'18 で最優秀論文賞を受けたのみならず，CAV'19（上述）や NFM'19 にも採択された．
その他，より理論的なトピックとして，確率的システムの静的解析手法としてのマルチンゲールの研究に取り組み，その成果をトップ国際会議 ATVA'18, TACAS'19 にて発表した．これらの手法を含む多様なシステム検証手法の論理的・圏論的基礎の研究もあわせて推進し，その成果の一つは理論計算機科学の旗艦国際会議である LICS'19 に採択された．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
CAV, EMSOFT, LICS, TACAS, ATVA 等のトップ国際会議において論文を出版し，学術界におけるインパクトの高い成果を上げることができた．さらに，これらの研究進展は理論から産業応用へ急速に裾野を広げつつあり，産業界の5社あまりと協働を行っている．
|
| 今後の研究の推進方策 |
引き続き，メタ理論と産業応用の両輪を推進力とした形式手法研究を推進する．特に，統計的機械学習との協働をより強力に推進する．
|
| 次年度使用額が生じた理由 |
（理由）
予定していた海外出張でとりやめたものがあった．
（使用計画）
次年度の予算と合わせ使用する．
|
