プログラミング言語やオペレーションシステム（OS）などの研究・実用化が進んできたおかげで、ソフトウェア開発技術は大きく発展してきました。しかしながら、より高度で複雑・大規模なソフトウェアを開発しなければならないという社会的要請はますます大きくなり、ソフトウェアの開発技術はそれに追いついていません。むしろソフトウェア開発技術は、他の工業製品や建造物などの設計・製造技術に比べるとまだまだ未発達の段階です。

本研究室では、形式手法を基にしたシステムの要求から仕様、設計に至るソフトウェア開発手法に関する研究開発を行っています。「形式手法」という言葉はなじみが少ないかもしれませんが、その心は、「開発するシステムをきっちりと分析し、システムの要求定義・仕様記述・設計の文書を厳密に記述することにより、ソフトウェア開発の見通しを良くしましょう」ということです。ソフトウェア開発における中心的な作業は「記述である」と言っても過言ではありません。形式手法は、対象システムの厳密な記述と解析を行うための道具立てを与えてくれます。しかしながら、形式手法を導入すれば、どのようにしたら要求が獲得でき、仕様が構築できるかという問題が解決されるわけではありません。

本研究では、システムの問題領域（要求）、問題を解決するための手段（仕様）、その実現方法（設計）に関し、それを支援するための要素技術の開発と要求・仕様・設計の記述を関連づけて、システム設計を一貫して体系的に行うための土台を築き上げます。形式仕様言語としてZやVDMを中心として、モデル化手法、プロトタイピング技術、仕様の検証技術、仕様の変更に関する技術や既存の開発手法との融合、図式表現との融合を図ります。

「形式手法」では、プログラムの検証と形式仕様記述の基礎を学びます。プログラムの検証では、プログラムの正しさとそれを保証するための方法を紹介して、「正しい」という意味を考察します。また、形式仕様記述では、プログラムの仕様を、数学の概念を用いて簡潔かつ厳密に記述する方法を、ZやVDM等を用いて具体例を通して習得します。