2013年4月24日情報システム学専攻・ソフトウェア論講座
結縁・寺内研究室
本研究室では、ソフトウェアを数理的手法によって検証することを目的とした基礎理論と検証手法を研究しています。社会のあらゆる部分に用いられるコンピュータを目的に応じて動作させるためソフトウェアは複雑化し、大規模化しています。ソフトウェアが正しく動作しているかどうかをテストによって確かめることは非常に難しくなりつつあります。このため、情報システムが複雑化・大規模化するに従って予期しない不具合が発生し、社会的に大きな影響を与えることが増えています。
このような問題に対して、入力データに対する出力の正しさを確かめる従来のテスト手法では、振舞いの正しさを保証することは実際的は不可能になりつつあります。このような問題を解決するために、ソフトウェアを構成するプログラムそのものを解析の対象とすることによって、数理的手法を用いることでソフトウェアの正しさを証明できれば、ソフトウェアの信頼性を飛躍的に高めることができます。また、そのような手法を明らかにすれば、正しいプログラムの構成技法やプログラミング言語設計の妥当性を議論することができるようになります。
このようなプログラムに対するソフトウェア科学は多岐にわたっており、そのソフトウェア、プログラムの性質に応じて研究する必要があります。本研究室では以下のようなプログラムを対象として、バグのないソフトウェアのための基礎理論と検証手法を研究しています。
- 並行・実時間ソフトウェア
外部環境にリアルタイムで対応し動作する実時間プログラム、複数のプロセスが同時に動作する並列分散システムなど、複雑な振る舞いをするソフトウェアを解析・検証するための基礎理論と検証手法について研究しています。
(図：並行計算モデルに基づくAIBOソフトウェアの動作検証)
- ソフトウェアモデル検査に基づくプログラム検証器
近年高い関心を集めている「ソフトウェアモデル検査」の技術を発展させ、ML など関数型言語やJava などオブジェクト指向言語に対するプログラム検証器を開発しています。
(図：述語抽象と抽象詳細化によるソフトウェアモデル検査)
以上のようなソフトウェアは、プログラミング技術の発展、ネットワーク技術の発展、組込みシステムによるユビキタス計算の展開によって、急速に発展した分野です。従来のソフトウェア構成技術の延長では、求められる信頼性を確保しながら、システムが持つ能力を十分に活かすことが難しくなっています。プログラムに対する論理、代数などの数理的概念を利用して、複雑なソフトウェアが不具合を起こすことなく動作することを検証するための方法論を科学します。