情報工学科
垣内 洋介
教員紹介
プロフィール
- 【専門分野】
- ○ハードウェア／ソフトウェアの機能検証と設計自動化
- 【担当科目】
- コンパイラ 、 オペレーティングシステム 、 組込みソフトウェア など
- 【研究テーマ】
-
1.ハードウェアの形式検証 高い信頼性が要求されるハードウェアの正しさ保証を、計算機によって行う技術の研究。
2.シミュレーションベース検証 大規模化するハードウェア／ソフトウェア設計の検証をシミュレーションによって効率よく行う技術の研究。
3.要求仕様解析 設計の元となる要求仕様から有用な情報を分析・抽出し、後の工程に役立てる技術の研究。
- 【ひとこと】
自分の流儀が通用しないところに積極的に出ていくことが、新しい自分の発見・開拓につながります。ぜひ、いろいろチャレンジしてください。
研究紹介
垣内 洋介KAKIUCHI Yosuke
情報学部 情報工学科 准教授
システムの堅牢性・安定性を高めるため、
テスト工程を「自動化」できないか。
PROLOGUE
今や金融でも医療でも、あらゆる分野にコンピュータシステムが入ったおかげで便利になりました。コンピュータのゲームだって面白くなっているし。それだけに、システムが何らかのエラーを起こしてしまうと、ゲームが動かない、ATMでお金が引き出せないなど、大問題です。システムがエラーを起こさないよう、開発会社は十分テストを行っているのですが、このテストに膨大な手間と時間がかかっています。そこで何とかシステムテストを自動化できないか、と研究しているのが垣内先生です。
プログラムをモデル化して解析。テスト工程の手間を大幅に削減
今やITは社会の隅々に浸透しており、システムを利用していない業界を探すのが難しいほどです。私たちの日常を便利で快適にしてくれるこれらのシステムが、エラーで故障すると大きな社会問題になってしまいます。故障に強く、堅牢で安定したシステムが、ますます求められているのです。
システム開発は通常（１）要求分析（２）全体設計（３）詳細設計（４）コーディングの順に進みます。よく言う「プログラミング」とは４の段階です。その後はテスト工程となり（５）単体テスト（６）統合テスト（７）システムテストと進み、ようやくシステムが完成します。
工程がかなり進んだ段階で出たエラーやバグは致命的です。場合によっては数千万円もの修正コストがかかってしまうことも珍しくありません。また、重要なシステムほど複雑で規模が大きくなる傾向があります。一般に（５）～（７）のテスト工程で、開発全体の３～８割もの時間と手間を費やしており、人海戦術でテストを行うのももはや限界です。そこで私は、テストを自動化できないかと考えています。
現場では、プログラムを実際に走らせて結果を見るテストがよく行われるのですが、これでは時間がかかってしまいます。私が研究するのは、プログラムをモデル化して充足可能性判定問題（SAT）と呼ばれる数式に置き換え、解析プログラムにかけてバグの有無を判定する手法です。実現するには、的確で効率的なモデル化が欠かせません。
テスト工程に全体の3～8割が費やされます
要求分析の段階で発生するバグを自動で取り除くには？
早い段階で発見されたエラーやバグは、修正も比較的容易です。ならば（１）の段階、つまり要求分析の段階でも、自動検証を取り入れればいいのではないでしょうか。
なぜ今までそれができなかったかと言うと、要求仕様が「曖昧」だからです。この段階では、顧客の要望を中心に仕様をまとめていきます。しかし人間の言語は曖昧で、モデル化が難しく、コンピュータによる自動処理に向きません。
ですが最近は、UMLやSysMLといった、要望を図式化できるフレームワークが登場しています。図式化が可能なら、自動テストも実現できる可能性があります。「要望（言語）を図式（モデル）に置き換える」のは、人間にしかできない、専門的なテクニックを必要とするプロセスです。この点に手間をかけておけば、顧客の要望がどのように実現されるのか、流れに矛盾がないか、コンピュータで自動解析できます。
モデルをしっかりと作り、それをシステムやプログラムに落とし込むこの手法をモデルドリブンアーキテクチャー（MDA）と呼びます。最初の段階でバグが解消されていれば、後工程がスムーズに進むのは言うまでもありません。
ここではサンプルとして
「コピー機を開発する場合」
の図式を表しています
「モデル化して自動解析」の手法は多方面に応用できる
「現象をモデル化してコンピュータに解析させる」というやり方は、いろんな場面に応用が利きます。私のもう一つの研究テーマである「数理最適化」でも、この手法が役に立っています。
例えば100人のプログラマで１つのシステムを開発しようという場合。能力の異なるプログラマをどう役割分担し、どんなスケジュールで業務させるかといったことは、プロジェクトマネージャーの頭を常に悩ませる問題です。
そこで、プログラマの能力を数値化し、システムに自動で割り当てさせるのです。こういった、ありとあらゆる選択の可能性があって最善策を見出すのが難しい時、モデル化してコンピュータに解析させ、一番よい道を探し出す「数理最適化」の技術は、様々な場面で応用できます。
人間社会に導入・活用されるシステムの規模や種類は、拡大する一方です。それに応じて、効率性と確実性の高いテスト手法がますます求められるでしょう。そうした期待に答えるため、さらにレベルアップを図っていきたいですね。
業務を自動で割り当てさせる数理最適化の例