セミナーレポート

情報化社会に必須のソフトウェア検証
について講演

「JAISTシンポジウム2011」を取材

このエントリーをはてなブックマークに追加

2011/11/28

 北陸先端科学技術大学院大学(JAIST)は2011年11月11日に「JAISTシンポジウム2011」を行った。このシンポジウムはJAISTが研究成果を紹介・発表するというもの。同大学の片山卓也氏は冒頭のあいさつで、現在は経済問題をはじめ困難な時代だと説明。「20年前、本学はこういうときに大変重要となる幅広い学力をもった人材を育成するために作られた」として、先端科学技術における研究をベースに、組織的な教育で人材育成を行っていることを改めて説いた。

真剣に話を聞く会場の様子
真剣に話を聞く会場の様子

JAISTが行うソフトウェアの研究


 JAISTは、2010年4月にソフトウェアの検証について専門的な研究を行う「ソフトウェア品質センター」を立ち上げた。


 ソフトウェアは社会基盤であり、そのため安全性と信頼性の確保が最重要課題だ。例えば電子商取引のネットワークでは常に安全なサービスの提供が欠かせない。自動車の「走る」「止まる」など、走行系の機能を制御するソフトウェアでも同様だ。そのため「ソフトウェア品質センター」では、社会基盤となっているソフトウェアが安全性と信頼性を担保できているかを検証する方法について研究を進めている。


 ソフトウェア検証研究センター・センター長の二木厚吉氏は、自身が中心となって行って研究している「CafeOBJ証明スコア法」という検証方法を提示。「CafeOBJ証明スコア法」は、開発段階での使用を記述するための言語システム「CafeOBJ」を利用した検証方法だ。二木氏は「この新しい仕様検証を利用することで、ソフトウェアを実用した段階で発覚するような問題点の検証が可能になる」として、さらに研究を進めていきたいとした。


ソフトウェアのモデル検査


 一方、東京大学情報理工学系研究科教授の萩谷昌己氏は、クラウドコンピューティングにおけるミドルウェアの検査手法について言及した。


 萩谷氏はハードウェア設計時に利用される「モデル検査」をソフトウェアに適用する「ソフトウェアモデル検査」を提唱。モデル検査とは、ハードウェアなどの設計について、数学を用いて検査を定式化(アルゴリズム化)して検証する方法だが、「ソフトウェアモデル検査」は、ソフトウェアに対しての“全てのふるまい”をアルゴリズム化して、検証する。


 そもそもソフトウェアは、一定の“状態”(数値が入力されるなど)に対して、動作(計算をするなど)が開始され次の状態に移行(遷移、という)するという一連の「ふるまい」でできている。「ソフトウェアモデル検査」とは、ソフトウェアをプログラムする上での「ふるまい」を数学的にアルゴリズム化をすることで網羅的な解析を可能にし、ソフトウェアが要件を満たしたかどうかを検証するというもの。


 萩谷氏は「クラウド上で扱うネットワークソフトウェアは互いに通信を行い多数のプロセス、言語が存在するため(ふるまいが開始される起点となる)“状態”が爆発的に増えている。状態爆発への対応策を考える必要がある」と展望を示した。

東京大学情報理工学系研究科教授・萩谷昌己氏   JAIST教授・小川瑞史氏

東京大学情報理工学系研究科教授
萩谷昌己氏

  JAIST教授・小川瑞史氏

ソフトウェア検証について


 JAIST教授・小川瑞史氏はソフトウェア検証について説明した。ソフトウェア検証とは、システムやプログラムと、満たすべき性質の双方をプログラムによるチェックが可能な形で記述することである。ところが、検証については人間の手が介在する以上、間違える可能性があり、完全なチェックは難しい。小川氏は「チェックの完全さは、コストとのトレードオフである」と説明する。


 さらに小川氏は現在のソフトウェア検証についてハードウェア的な限界も言及する。例えば現実のソフトウェアのコードは全体で数百万行~数千万行にも上るのに対して、現在コンピュータの自動的な検証に使える規模は数万行~数十万行という範囲だという。小川氏は「産業側からこうした問題を抽出し、大学側からの手法、問題の解決方法を提示できるような産学連携などをいかに行っていくかが鍵になる」と話した。


 ソフトウェアを正しく機能させるためにはソフトウェア検証が当然必要だ。しかし、それをいかに正確に行っていくことで安心して運用できるようにするかが課題となる。こういった研究をJAISTが引っ張っていくことで、より正確なソフトウェア運用が行われていくことを期待したい。

(山下雄太郎)

【セミナーデータ】

イベント名
:JAISTシンポジウム2011
主催   
:北陸先端科学技術大学院大学(JAIST)
開催日  
:2011年11月11日
開催場所 
:富士ソフトアキバプラザ(東京都千代田区)

【関連カテゴリ】

IT政策