教員	部屋番号	内線
西澤 弘毅	6-418（教員室）	3378（教員室）
	6-306（研究室）	3343（研究室）

研究室内容

現在、情報システムは、原子力発電所などの大規模な施設から自動車や家電など身のまわりのものまで、さまざまな物の中で動いています。これらがもし誤った動作をしたら、我々の生命や財産が脅かされることになります。 作った情報システムが決して誤った動作をしないということを保証するには、数学的な手法が役立ちます。そのような数学的な手法でシステムを検査することをシステム検証と言います。この研究室では、システム検証を行ったり、システム検証に役立つ論理や代数などの数学的手法を研究したりします。

しかし、原子力発電所や自動車などの複雑なシステムを、いったいどうやって検証したらよいのでしょうか。実際には、世の中にあるシステムやプログラムをそのまま検証するとは限らず、検証に必要な部分を抜き出す「モデル化」という作業をして、そのモデルを自動的に検査することが多いです。モデルとは、数式や文字列だったり、ここに示したような図だったり様々です。システム検証を病院の健康診断に例えると、モデルとはレントゲン写真みたいなものです。

研究室のコンセプトは「暗黙の前提や常識を疑うこと」。たとえ他人が当たり前に思うことでも、自分が確信を得るまでとことん考えないと気が済まない人は、ぜひこの分野を研究してみてください。