2017 Fiscal Year Research-status Report
圏論と数理論理学によるものづくりサポート―ソフトウェア科学のシステム工学への移転
| Project/Area Number |
15KT0012
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
蓮尾 一郎 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (60456762)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Project Period (FY) |
2015-07-10 – 2019-03-31
|
| Keywords | 物理情報システム / モデルベース開発 / 形式検証 / ハイブリッドシステム / 数理論理学 / 圏論 / プログラム理論 |
|---|
| Outline of Annual Research Achievements |
ソフトウェア科学における諸手法のシステム工学への応用という最終目標に対して，多様なトピックにおいて大きな進展があった．
まず，ソフトウェア科学におけるモデル検査手法のトピックについて，この圏論的本質を明らかにする理論的成果を理論計算機科学分野の旗艦国際会議および圏論的代数・余代数分野の主要国際会議において予稿集論文として発表した [Urabe, Hara & Hasuo, LICS’17], [Cirstea, Shimizu & Hasuo, CALCO’17]．
また，連続量を扱う物理情報システムにおいて，検証や自動生成等のさまざまな問題を解くにあたっては，もともとの問題を連続量最適化問題に帰着して解くのが定石である．多項式補完という重要な論理的問題を半正定値計画問題に帰着する手法について，特に最適化ソルバーの数値誤差に対処するための手法を提案した成果を，国際会議予稿集論文[Okudono et al., APLAS’17] として発表した．
さらに，実行時モニタリングのトピックについても大きな進捗があった．複雑でかつブラックボックス・コンポーネントを含むために従来の意味での「検証」が難しい物理情報システムに対して，特に産業界から大きな注目を集める手法が実行時モニタリングである．時間付きオートマトンの理論を用いて，実時間制約を含む仕様に対して実行時モニタリングを行う手法を提案し，この成果を国際会議予稿集論文[Waga et al., FORMATS’17] として発表した．
上記成果の産業応用について，複数の企業と議論を開始し，現在継続中である．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
複数の企業との協働を通じた実問題の検討と，形式手法の理論的研究，さらに形式手法のメタ理論たる数学的研究，以上の三者の有機的な結合が実現されており，総体としての研究活動が想定以上のペースで進んでいる．
|
| Strategy for Future Research Activity |
引き続き，メタ理論と産業応用の両輪を推進力とした形式手法研究を推進する．
|
| Causes of Carryover |
（理由）
予定していた海外出張でとりやめたものがあった．
（使用計画）
次年度の予算と合わせ使用する．
|
