ソフトウェアの仕様を，集合，関数，論理など数学的な考え方にもとづいて記述し，検証するための技術である，形式手法 (Formal Methods) という研究分野です． 昨今ソフトウェアに起因する事故が新聞等を賑わしていますが，形式手法はソフトウェアの信頼性を向上させる手段として最も注目されています． Languageチームでは，この形式手法に基づいたソフトウェアの設計検証についてArchfaceと呼ばれるインターフェースを通して研究を行っています．
Archfaceとは鵜林先生を中心としたModelsチームで開発を行っている設計と実装を関連付けるインターフェース機構です． Archfaceを用いることで設計モデル同士の整合性，コード同士の整合性，また，設計とコードのトレーサビリティを保ちながらプロジェクト開発ができることを目的として研究を行っています． また，Archfaceを効率よく，かつグラフィカルに扱うためにiArchという統合開発環境をEclipseのプラグインとして開発しています．
ソフトウェア工学，形式手法，設計検証，UML，アスペクト指向
