新着情報 テーマカテゴリ 全カテゴリバイオテクノロジー医学・薬学農林水産・食品環境・エネルギー素材機械情報・通信エレクトロニクス航空・宇宙大気・海洋経済・経営・政策・法律土木・建築社会・文化・教育基礎科学 ごあいさつ ご利用にあたり 検索方法 プライバシーポリシー ご意見・ご質問 実例集 見つからない場合は? DUCRホームページへ トップページ geta_logo
print
印刷時に縮小されてしまう場合などにご利用ください。

整理番号 7169   (公開日 2016年08月02日) (カテゴリ 機械情報・通信エレクトロニクス基礎科学
工業製品の高信頼化・効率化のためのソフトウェア科学的手法
●内容  ソフトウェア科学では《検証》(プログラムやシステムが仕様(=特定の望ましい性質)を満たすことの数学的証明を与える)や《自動生成》(仕様をみたすためのシステムのパラメータやシステム自身を自動的に探索し生成する)の手法が数多く研究されている。このようなソフトウェア科学手法の従来の対象は離散的・デジタル的なソフトウェアであった一方で、近年の計算機利用環境の多様化に伴い(自動車、生産システム、電気製品、スマートグリッド、ロボティクスなど)、ソフトウェア科学的検証・自動生成手法の《ヘテロジニアス化》がさかんに追求されており、物理系に起因する連続ダイナミクスや、確率・実時間性・コスト等の定量的性能指標を取り扱えるような手法が提案されつつある。
 また、上記のような潮流の中で、機械学習等を応用し現実のシステムの規模に対応するスケーラビリティを持った《軽量形式手法》や、現場のエンジニアによる活用を促進するような《可視化・ユーザーインターフェース》の研究も進んでいる。
 この研究グループでは、ソフトウェア科学的手法に対する(圏論や論理学による)《数学的メタ理論》を構築することで、上記のようなヘテロジニアス化のワークフローを加速することを目指している。検証・自動生成等のソフトウェア科学的手法の応用に関心を持つ企業との共同研究を通じて、この手法の産業応用、及び産業界の問題に牽引される形でのさらなる理論研究の進展をぜひ行っていきたい。
●研究者
准教授 蓮尾 一郎
大学院情報理工学系研究科 コンピュータ科学専攻
●画像


クリックで拡大

検証の例: プログラム論理
(C) 蓮尾 一郎

自動生成の例: 制御器自動生成
(C) 蓮尾 一郎
mail
上記内容は、各研究者へのインタビューをもとに東京大学 産学協創推進本部で骨子をまとめたものです。
本件に関する共同研究等のお問い合わせは、左のバナーをクリックしてください。スタッフがお問い合わせをお受けいたします。