このページの先頭です

メニューを飛ばして本文を読む

ここから本文です

サイト内の現在位置

研究者情報:研究・産学連携

研究室紹介OPAL-RING
田原 研究室

高品質なソフトウェアを速く、安く、正確に作る

所属 大学院情報システム学研究科
社会知能情報学専攻
メンバー 田原 康之 准教授
所属学会 情報処理学会、日本ソフトウェア科学会
研究室HP http://www.ohsuga.is.uec.ac.jp/~tahara/
印刷用PDF

掲載情報は2015年8月現在

田原 康之
Yasuyuki TAHARA
キーワード

ソフトウェア工学、形式検証(モデル検査)、要求工学(ゴール指向要求分析)、セキュアなシステムの開発手法、ソフトウェア基礎理論(カテゴリ理論、代数モデル、形式的意味論)

現代のモノづくりはソフトウェアが鍵を握っているといっても過言ではありません。携帯電話やデジタル家電、自動車、医療機器などには「組み込みソフトウェア」が内蔵されています。ハードウェアに対して、ソフトウェアはプログラムによって書き換えられるため、機能の追加や変更が容易です。ソフトウェアの導入によってモノづくりは高性能化し、開発スピードも格段に向上しました。
しかし、ソフトウェアは近年、大規模化が進み、プログラムが複雑化してソフトウェア開発に必要なコストが膨らんでいます。ソフトウェア産業では人海戦術で乗り切る傾向が見られますが、それも限界があります。大勢のチーム作業はマネジメントも難しく、刻々と移り変わる市場ニーズも常にくみ取らなくてはなりません。
これらの課題を解決する学問が「ソフトウェア工学」です。ソフトウェアをいかに速く、安く、高品質に作るか――。ソフトウェア工学はこうした目的を達成するため、数理論理学などの高度な数学の理論を駆使し、有益なソフトウェアの開発を目指すアプローチです。プログラムの作成には人間の知的活動が深く関わっています。そのため、心理学などの人文・社会科学とも決して無縁ではありません。
ソフトウェアは人間がプログラミングして作るため、曖昧な部分が多く、そこに間違いがあればバグ(欠陥)となって装置の誤動作などを引き起こします。人間の曖昧さと、記述通りのプログラムでしか動かないコンピュータとの間に大きな溝があるのです。
従来は複数の目でチェックしたり、テストデータを入力したりして動作を確認していました。しかし、プログラムのすべての動作をチェックすることは現実的ではありません。そこでソフトウェア工学の手法を使って、厳密な数学の理論に基づいてプログラムの正しさを網羅的に確認するのです。
ソフトウェア工学が専門の田原康之准教授は、ソフトウェアの仕様の記述や設計、検証のための「形式手法(Formal Methods)」と呼ばれるツールを使っています。その中でも特に、ソフトウェアの仕様に対して網羅的かつ自動的にプログラムを検査する「モデル検査」手法を使いこなすエキスパートです。
具体的には、グーグルマップなどに使われているウェブアプリケーションの代表的な開発手法である「Ajax(エイジャックス)」にモデル検査を適用する研究を行っています。Ajaxは操作性が高い反面、動作が複雑でバグが発生しやすい問題点があります。田原准教授はAjaxに初めてモデル検査を導入し、プログラムのバグをほぼ自動で迅速かつ正確に見つけ出すことに成功しました。

モデル検査は一部で実用化されつつある手法ですが、今後、Ajaxなどの汎用技術に本格的に導入されれば、その方式が瞬く間に普及するでしょう。実用に向けて超えるべきハードルはまだいくつもありますが、「数学は無限の領域を理論的に扱える。数学を活用したツールを使えば、要求通りに動くソフトウェアが作れる。プログラムのバグが減り、短納期かつ低コスト化の厳しい顧客要求にも応える、高品質なソフトウェアが作れるだろう」と田原准教授は期待しています。

進歩の速いソフトウェア産業では、高度な技能を身に付けた技術者が不足しています。田原准教授は国立情報学研究所(NII)が推進している、社会人向けのソフトウェア技術者養成プログラム「トップエスイー」の立ち上げに関わり、発足時から現在に至るまで長らく講師を務めています。
日本でこれだけ充実したIT教育プログラムは他にはないそうです。田原准教授は「現場の技術者に日進月歩の技術を習得してもらい、すぐにその専門技術を現場で発揮してもらいたい」と考えています。実際に、大手メーカーの技術者が数多く受講し、企業のモノづくりに生かされています。また、電気通信大学とNIIは提携関係にあり、「トップエスイー」の修了者が電通大の博士課程に進学するといった好循環も生まれつつあります。
【取材・文=藤木信穂】 

研究・産学連携