ソフトウエア科学領域【二木研究室】
■言語
言語は人間の情報処理や知的活動の根本を担うとされます。最近のJava言語やXML言語の例を引くまでもなく，コンピュータやネットワークなど，情報や知識の伝送／処理／蓄積のための科学技術の進歩は，新しい言語の出現によって支えられてきました。私の研究室の名前は言語設計学（Language
Design）で，私自身はこの名前が気に入っています。普遍的でありながら常に斬新な研究のアプローチを示唆しているからです。
■言語設計
現実の問題に接するところには常にアプリケーション（略してアプリ）と呼ばれるシステム／ソフトウェア／プログラムがあります。ゲームソフト，文書処理ソフト，電子商取引システムなどはすべてアプリです。こうしたシステムは使用者とそのアプリ特有の言語を使ってコミュニケーションしています。このアプリと使用者（人間）のコミュニケーションを分析し，そのための言語を設計することで，より使いやすく信頼性の高いアプリを作ることが出来ます。
■フォーマルメソッド（Formal Methods）
問題をコンピュータやネットワークを使って解決するためには，その問題解決の要求を分析してモデルを作り，その実現可能性やコストを評価する，といったことが必要です。こうした新たな問題のモデル化と分析には，その問題特有の言葉（vocabulary）を整理し，それを使って問題のモデルを記述し，そのモデルに基づき問題に関係している色々な人々と意思疎通を図りながら，モデルを精緻化しつつ問題の分析を進める，といった活動を行うことになります。こうした活動の中心には，新たな言語を設計することがあり，言語設計はシステムの設計開発で大変重要な役割を担うことになります。こうした考え方は，現在のシステムの設計開発の現場では一般的ではありませんが，フォーマルメソッドとよばれる数学モデルに基づくシステムの設計開発法の中心にはこの考え方があります。
■CafeOBJ
CafeOBJは問題のモデルや仕様を記述するための新しいタイプの計算機言語です。
CやJavaといったプログラムを書くための言語ではなく，問題をより人間に近いところでモデル化／定式化して，プログラムを書く前に問題について考えたり分析したりするための言語です。CafeOBJは問題ごとに新しい言語を定義するメタ言語（Meta
Language）としての機能も備えているので，上で述べたフォーマルメソッドの中心となる言語設計をするための言語でもあります。CafeOBJ言語とそのシステムは，10年以上にわたる多くの人々との協力による国際的な活動の中で，二木研究グループが中心となって研究開発してきました。
■研究テーマ
二木研究室では，現在のCafeOBJ言語システムを使用しつつ，またそのあるべき将来像を探って，以下のような研究を展開しています。
システム検証技術とそのシステム化：より分かりやすく使いやすいシステム検証技術としての簡約（reduction）のみを用いた検証法とそのシステム化。
社会システムのモデル化と解析・検証：政府・自治体組織や会社組織といった社会システムやドメインのモデル化と解析／検証。
安全プロトコルのモデル化と解析・検証：電子商取引プロトコルなど電子社会の基盤となる安全プロトコル（secure protocol）のモデル化と解析。
アプリケーションモデルの形式化と解析・検証：エージェントシステムなど各種のアプリケーションモデルの形式モデルとその解析・検証法。
バイオシステムのモデル化と解析・検証：細胞内での化学反応の記号的なモデル化と解析など，システムバイオロジーへのフォーマルメソッドの適用。
■代表的な著書・論文
- Verifying Specifications with Proof Scores in CafeOBJ, Proc.
of ASE2006, pp. 3-10, 21st IEEE International Conference on
Automated Software Engineering (ASE '06), 2006. (invited paper)
- Verifying Design with Proof Scores, Proc. of 1st IFIP-WG2.3Conf
on VSTEE (electric form), October 2005.
- Logical Foundations of CafeOBJ, Theoretical Computer Science,
285, pp.289--318, 2002.
- Formal Methods in CafeOBJ, Lecture Notes in Computer Science,
2441, pp.1-20, 2002. (invited paper)
- CafeOBJ Report: The Language, Proof Techniques, and Methodologies
for Object-Oriented Algebraic Specification, World Scientific,
AMAST Series in Computing 6, 1998.
