本研究室では，以下の内容について研究を行なっています．
ソフトウェアテスト
ソフトウェアテストとは，ソフトウェアに不具合があるかどうかを検査するものです．テストの対象となるソフトウェアに値を入力しその出力が正しいかどうかを判断します．入力する値は1つではなく，複数の値の組み合わせによって行われることが多いです．このとき，この入力する値の組合せをテストケースと呼び，それを用いて行うテストを組合せテストといいます．
テストケースの数が少ないとテストを実行する回数も少なくなりますが，ただ単純に数を減らすだけでは，不具合を見逃す可能性があります．そこで，数を減らしつつ，不具合を検出しやすい，効率的なテストケース生成方法について研究を行っています．
自己適応システム
自己適応システムとは，あるシステムが周囲の環境を観測し，変化に伴って自らの振舞いを環境に適応することができるシステムです．システムが観測する環境は様々です．通信に関するものならば，通信量，通信速度，アクセス量などが挙げられます．また，自動運転システムでは，自車の速度，燃費，周辺の車や歩行者などの場所などが挙げられます．
多くのソフトウェアシステムは，この様になればこの様にする，が事前にプログラムとして組み込まれています．しかし，周辺の環境や自身の環境が変化すると，この様になってもこの様にできない，この様になったけど別の方法でしたほうが効率がよい，ことが考えられます．
環境の変化は，ソフトウェアシステムに対する入力の変化と考えることができます．自身が使うセンサなどの故障が発生すると入力される情報が得られない，入力される情報が突然増加した，新しいセンサを設置したため新規の入力が追加されたなどです．
ここで，自己適応システムの考え方を用いることで，周辺の環境が変化したとしても，新しくソフトウェアシステムの設計や実装をやり直すことなく継続して使用することが可能になります．この様な自己適応システムをどのように設計するか，自己適応システムを実現しやすいフレームワークはどんなものか，について研究を行っています．
モデル検査
モデル検査とは，あるシステムが仕様などに定義された満たすべき特性を満たしているかどうかについて数学的に検証します．多くの場合，モデル検査はシステム開発の設計などの工程で行われ，プログラム設計や実装に入る前に，これから作るものが特性を満たしているかどうかの検証を行います．実装を行っている途中に特性を満たしていないことがわかると，改めて設計をやり直すなど，コストや開発期間の増加を引き起こす可能性があるからです．
モデル検査は，ツールを使って行われることが多く，そのツールで利用できるように検証したいシステムをモデル化します．そして，検証する特性もそれに合わせてモデル化し，検証を行います．検証するシステムをそのままモデル化してしまうと，検証時に非常に多くの計算時間が必要になり検証が完了しないことがあります．
モデル検査を行うにあたって，対象となるシステムを効率よく検証するためにどのようにモデル化するか，計算時間を現実的な時間以内に終えるにはどうするか，などツールの改良やモデル化手法の研究を行っています．
ゴール指向要求分析手法
あるサービスを提供するシステムを実現するにあたって，そのサービスが何を提供するか，そのためにどのような手続きが必要かを明確にする必要があります．例えば何が入力で何が出力なのか，誰がどの操作をどの様に行うのか，物理的にどこに置くのか，ユーザがこのシステムに期待することは何か，など数多くのシステムの機能や要件を“要求”として洗い出します．しかしインタビューなどで収集される要求は曖昧であることが多いため，クライアントとデベロッパの間で認識のずれが生じる可能性があります．
この曖昧な要求を具体化するための手法の1つとして，ゴール指向要求分析手法があります．これは，最終的なゴールを細分化し階層化したモデルを構築することで，より具体的な要求を獲得します．しかし，要求を漏れなく取り出すことやモデルを正しく構築することは困難であるため，適切なゴールをどのようにして取り出すか，取り出したゴールをどう接続するかなどの研究を進めています．
経路保証プロトコル
経路保証プロトコルとは，ある２つの端末間の通信経路が正しいことを保証するプロトコルです．対象となるネットワークは無線マルチホップネットワークです．センサネットワークやモバイルアドホックネットワーク，車車間ネットワークなどが挙げられます．これらのネットワークでは，端末の移動や増減により特定の通信経路を維持することが難しいため，通信毎に経路を構築したり，定期的に経路が存在するか確認して無ければ構築しなおす様にして端末間の通信を行います．無線通信なため，通信範囲に入れば誰でも電波は受信できますし，端末に対して電波を送信することができます．そのため，端末間で経路を構築している際に，悪意ある人物が偽の経路情報をネットワークに流すことが可能となります．経路保証プロトコルでは，たとえ偽の経路情報がネットワークに流れたとしても，それが偽物だと判別して経路を適切に構築することが可能となります．
経路保証プロトコルでは署名を用いて経路の正しさを証明しています．実際に署名方式を実装し経路保証プロトコルとして実装し，署名の生成や検証時間，経路が構築される様子を計測し性能評価を行なっています．
