並行自己反映計算による
安全な動的適応

今日、コンピュータは様々な機器に組込まれており、それらの動作環境は刻一刻と変化します。そのようなコンピュータ上のプログラムは動作環境の動的な変化を考慮して作成する必要があり、結果として複雑になりがちです。現在まで渡部研究室では、自己反映計算にもとづく動的適応機構が、環境の変化に強くセキュアなソフトウェアの構成に貢献できることを示してきました。現在は、関数リアクティブプログラミング(FRP)やアクターモデルにこの考え方を取り入れ、安全で適応的な組込みシステムの構成方式について研究を行っています。

形式手法にもとづく
セキュアなシステム構成方式

プログラムのみたすべき性質を論理や代数に基づいて曖昧さのないよう記述し、プログラムの品質向上を目指す方法論を形式手法と呼びます。渡部研究室では、並列計算システム上のソフトウェアの安全性向上に向けて、並行計算モデルのひとつであるアクターモデルのための形式検証手法を提案しています。また、人間の作業手順の記述（手順書）が、どのようなヒューマンエラーに対して頑健であるかといった、プログラミング以外の領域に対する形式手法の応用研究も行ってきました。現在は、関数リアクティブプログラミング(FRP)にもとづく組込みシステムのための形式検証手法に取り組んでいます。