2007年07月31日情報システム学専攻・ソフトウェア論講座
阿草・結縁研究室（阿草清滋教授 結縁祥治教授 小林隆志特任准教授 濱口毅助教）

　本研究室では、工学・科学双方からのアプローチによって、ソフトウェア開発における信頼性の向上および低コスト化を目標とした活動を行っています。実世界へ直接的に適用可能な基盤技術を工学的アプローチによって提供するとともに、計算機科学を基礎とした先進的な開発手法のための理論研究および応用について研究を行っています。具体的な研究項目は以下のとおりです。

● ソフトウェア開発環境

　プログラムを解析し各構文要素に意味を付加したソフトウェアリポジトリやソフトウェア関連文書を利用し、ソフトウェアの保守性・信頼性・生産性を向上させる開発環境について研究しています。

● 高信頼並行ソフトウェアの構築・検証

　並行計算理論に基づく高信頼な並行ソフトウェアを開発する手法について研究しています。主な研究分野は、プロセス代数、時間オートマトンなどの基礎理論、およびそれらの理論に基づくソフトウェアの構築および検証（操作的意味論、プログラミング言語、モデル検査、型理論など）です。
ソニーのエンタテイメントロボットAIBOのソースコードをモデル検査により検証し、デッドロックフリー性を保証する手法を開発しました。AIBOのシステムは並行に動作する複数のコンポーネントからなりますが、直接に相互作用しないいくつかのコンポーネント群に分割することで、検証における組み合わせ爆発の問題を軽減しました（図1）。

• 図1：AIBOソフトウェアモデルの分割検証

● 高信頼性WebWare生成技術

　ソフトウェア解析技術を基礎として、多様で複雑なWewWareの情報を統一的に管理するリポジトリの開発、開発・保守のためのワークベンチの構築について研究しています。本研究の応用例としてWebWareのページ遷移ビューを示します（図2）。
多種のプログラム言語で記述されたWebWareを統一的に表示することによって開発者は容易に検査を行うことができるようになります。

• 図2：ページ遷移ビュー

● 形式的ソフトウェア開発技法

　信頼性の高いソフトウェアの効率的な開発支援として、形式的仕様記述を利用したソフトウェアの移植、仕様記述・理解支援などについて研究しています。