ソフトウエアのバグがないことを証��してくれるツールをMonoidicsが拡販へ
半導��ビジネスにソフトウエアの比率が高まってくるにつれ、ソフトウエアプログラムにつきもののバグが頭痛の�|になる。これまでバグを���Eするツールは見つけて除去するだけで、他にも�遒鵑任い覯���性はあった。もし、バグがないことを証��してくれたら、SoCの設��時間がぐんと�]くなる。この夢を実現してくれるソフトウエアツールが普及の兆しを見せている。
英国ロンドンを拠点として日�櫃砲皀�フィスを��く、モノイディクス（Monoidics）社は、2�Q�iにロンドン�j学のピーター・オーハン教�bと�櫂�ーネギーメロン�j学のジョン･C･レイノルズ教�bが�]ち立てたプログラムの��しさを証��する理�bを�W��して、それを����化し商���@「Infer」と�@��けた。二人の教�bは今でもモノイディクス社の顧問でもある。
同社日本�Ъ劵妊�レクタであるRichard Rettig��によると、このツール「Infer」は世の中にあるC/C++で書いたプログラムならどれでも適��できるが、同社の狙う�x場は組み込みソフトの分野だという。組み込み�Uの�j��模なSoCやFPGAのプログラム開発ではC言語を使う例が�\えているからだ。
「Infer」のメリットは、コストを抑えたままバグのないソフトウエアプログラムを証��できる点である。これまでバグを除去する場合は、ソフトウエア����のプログラムをつぶさに調べると時間(コスト)がかかってしまうが、調�h����のプログラム�霾�を��らすと時間は�]くなるが、カバレージ（���垣�）が下がってしまいプログラムの����が落ちてしまう。できるだけ�]時間でバグのないことが証��できればありがたい��「Infer」は�]時間でバグを調べバグがなくなったことを証��するソフトウエアである。ただし、プロシージャ（プログラムの中で、繰り返し登場する処理を行うために�k連の命令を�kつの�}順(procedure）としてまとめたもの）レベルでのコードが�W��であることを証��する�lであり、プロシージャレベルではないコードに関しては��ずしも�W��という�lではない。
「Infer」は3つのソフトウエア����からなる。発見しにくいバグを捉えるBug Catchingと、�L陥のないことを証��するFormal Verification、ソフトウエアの����をビジュアルに表��するInferクオリティチャート、である。Bug Catchはソースコードの画�C�屬縫┘蕁爾�あるとそれをハイライトで表��し、Formal Verificationはプロシージャごとに証��ダイアグラムを発行する。Inferクオリティチャートでは、�T��の優先順位と、カバー率を表��しプログラムの����をビジュアル化する。
この中で、Formal Verificationツールと�}ばれるものは��来もあった。しかし、これまでのツールではプログラムコードをチェックし、バグのある所に優先度を��けそれぞれ直していくという作業が中心だったという��「Infer」のFormal Verificationツールは、バグがないことを数学的に証��するものであり、プログラムの����をチェックする時間を�]縮、すなわち検�hコストを下げることができる。
図1 プログラムの����を図で表�� 出�Z：Monoidics
Inferクオリティチャートは、ソフトウエアの����をCall Rankという指�Yと、証��の(プルーフ)カバレージという指�Yを使って表すもの(図1)。横軸のプルーフカバレージは0%から100%まであるが、�e軸のCall Rankはプロシージャが�}ばれる割合で、高い�気曚匹茲��}ばれていることを��す。�L陥のある�霾�を��、橙、黄でそれぞれ�Hい、中くらい、少ない、を表している。�L陥がないコードは�uで表す��図1の���笋曚��W��であり、左�笋柾L陥を含む可��性が�Hいことを表している。
「Infer」はコードとメモリとの関係をきっちり保証することが実現のカギだという。見つけにくいバグの中でもメモリリークと�}ばれる、メモリ�覦茲�徐々に��ってしまう現��に�咾�。メモリリークはOSのメモリ管理�桔，北筱�があったり、アプリケーションにバグが残っていたりすると��きやすい、と言われている。
「Infer」の�~�Wな点は、サードパーティのコードに�瓦靴討�����をチェックできることだ(図2)。経済�噞省の組込みソフトウエア�噞実��調�h報告書2010によると、世の中にある��てのソフトウエアの平均的なプログラム行数は99.8万行であり、そのうち��くゼロから開発するコードは45.4万行である。残りの54.4万行はソフトの再�W��ということになる。となるとサードパーティのソフトを流��することがごく�k般的になってきていることになる。ただし、「サードパーティのコードには����基��がない。その����基��は他のコードとの互換性もない」とRichard Rettig��は言う。また、サードパーティのコードがたとえ��しくても、組み合わせると�L陥となるケースもあるという。
図2 サードパーティのソフトのチェックにも�~効 出�Z：Monoidics
そこで、サードパーティも含めたソフトウエアの����をチェックするために、ドライバからライブラリ、ミドルウエア、アプリケーションの��てに渡ってチェックすることが��要になってくる。それもできるだけ開発の�嵶�工��で行い、バグを�����Zい工��まで�eっていかないことが�_要になる。��に、Androidデバイスに使われるソフトウエアはサードパーティだらけなので再�W��のチェックは不可�Lである。
このソフトの入�}�桔，箸靴�、PCやサーバーにインストールするパッケージソフトの他に、クラウドを�W��する�桔，眤靴┐討い襦�「Infer」はC/C++をサポートしているが、2012�QにはJavaプログラムにも�官�する予定だ。
