| 研究実績の概要 |
ソフトウェア科学における諸手法のシステム工学への応用という最終目標に対して，多様なトピックにおいて大きな進展があった．
まず，ソフトウェア科学におけるモデル検査手法のトピックについて，この圏論的本質を明らかにする理論的成果を理論計算機科学分野の旗艦国際会議および圏論的代数・余代数分野の主要国際会議において予稿集論文として発表した [Urabe, Hara & Hasuo, LICS’17], [Cirstea, Shimizu & Hasuo, CALCO’17]．
また，連続量を扱う物理情報システムにおいて，検証や自動生成等のさまざまな問題を解くにあたっては，もともとの問題を連続量最適化問題に帰着して解くのが定石である．多項式補完という重要な論理的問題を半正定値計画問題に帰着する手法について，特に最適化ソルバーの数値誤差に対処するための手法を提案した成果を，国際会議予稿集論文[Okudono et al., APLAS’17] として発表した．
さらに，実行時モニタリングのトピックについても大きな進捗があった．複雑でかつブラックボックス・コンポーネントを含むために従来の意味での「検証」が難しい物理情報システムに対して，特に産業界から大きな注目を集める手法が実行時モニタリングである．時間付きオートマトンの理論を用いて，実時間制約を含む仕様に対して実行時モニタリングを行う手法を提案し，この成果を国際会議予稿集論文[Waga et al., FORMATS’17] として発表した．
上記成果の産業応用について，複数の企業と議論を開始し，現在継続中である．
|
