研究室紹介
研究指導方針
こちらに本研究室における研究指導方針や修士学生の研究スケジュールなどを掲載しています．
本研究室を志望する方は参考にしてください．
研究テーマ
ソフトウェア形式手法分野で行われている研究です．
言語設計，フォーマルメソッド，CafeOBJ
教授 二木厚吉
言語
言語は人間の情報処理や知的活動の根本を担うとされます．最近のJava言語やXML言語の例を引くまでもなく，コンピュータやネットワークなど，情報や知識の伝送/処理/蓄積のための科学技術の進歩は，新しい言語の出現によって支えられてきました．我々の講座の名前は言語設計学(Language Design)で，私自身はこの名前が気に入っています．普遍的でありながら常に斬新な研究のアプローチを示唆しているからです．
言語設計
言語設計は多くの分野で重要な役割を演じています．コンピュータやネットワークが現実の問題に接するところには常にアプリケーション(略してアプリ)と呼ばれるシステム/ソフトウェア/プログラムがあります．ゲームソフト，文書処理ソフト，電子商取引システムなどはすべてアプリです．こうしたシステムは使用者とそのアプリ特有の言語を使ってコミュニケーションしています．このアプリと使用者(人間)のコミュニケーションを分析し，そのための言語を設計することで，より使いやすく信頼性の高いアプリを作ることが出来ます．
研究テーマ
問題をコンピュータやネットワークを使って解決するためには，その問題解決の要求を分析してモデルを作り，その実現可能性やコストを評価する，といったことが必要です．こうした新たな問題のモデル化と分析には，その問題特有の言葉(vocabulary) を整理し，それを使って問題のモデルを記述し，そのモデルに基づき問題に関係している色々な人々と意思疎通を図りながら，モデルを精緻化しつつ問題の分析を進める，といった活動を行うことになります．こうした活動の中心には，新たな言語を設計することがあり，言語設計はシステムの設計開発で大変重要な役割を担うことになります．こうした考え方は，現在のシステムの設計開発の現場では一般的ではありませんが，フォーマルメソッドとよばれる数学モデルに基づくシステムの設計開発法の中心にはこの考え方があります．
CやJavaといったプログラムを書くための言語ではなく，問題をより人間に近いところでモデル化/定式化して，プログラムを書く前に問題について考えたり分析したりするための言語です． CafeOBJは問題ごとに新しい言語を定義するメタ言語(Meta Language)としての機能も備えているので，上で述べたフォーマルメソッドの中心となる言語設計をするための言語でもあります．CafeOBJ言語とそのシステムは，10年以上にわたる多くの人々との協力による国際的な活動の中で，言語設計学研究室が中心となって研究開発してきました．
二木研究室では，現在のCafeOBJ言語システムを使用しつつ，またそのあるべき将来像を探って，以下のような研究を展開しています．
- システム検証技術とそのシステム化 :
より分かりやすく使いやすいシステム検証技術としての簡約(reduction)のみを用いた検証法とそのシステム化．
- 安全プロトコルのモデル化と検証 :
電子商取引プロトコルなど電子社会の基盤となる安全プロトコル(secure protocol)のモデル化と解析．
- UML(Unified Modeling Language)の意味定義と検証 :
ソフトウェアシステムのモデル化の共通図式言語となりつつあるUMLの意味モデルとその解析法．
- アプリケーションモデルの形式化と解析 :
エージェントシステムなど各種のアプリケーションモデルの形式モデルその解析法．
- 社会システムのモデル化と検証 :
政府/自治体組織や会社組織といった社会システムのモデル化と解析/検証にも取り組みたいと計画しています.
(詳細