コンピュータ理工学部 ネットワークメディア学科 平石　裕実 教授

ハードウェア＆ソフトウェアの自動検証

　私たちが普段使っているコンピュータは、精密な回路と巧妙なプログラムが組み合わさってできています。もしもその一部分でも壊れていたら、もちろん動くことはありません。では、コンピュータの故障を見つけるには、どうしたらいいのでしょうか？そこで登場するのが、数学や論理学に基づいた「検証」という分野です。回路の故障から設計のミス、プログラムのバグまで効率的に見つける、コンピュータ設計における検証の専門家である平石裕実先生に、最先端の研究内容を伺いました。

コンピュータの故障を見つける

　私たちが普段使っているコンピュータは、ハードウェアとソフトウェアに分けることができます。ハードウェアはコンピュータの本体、ソフトウェアはその上で動かすプログラムだと思っていただければいいでしょう。

　コンピュータの大本となるハードウェア。それを構成しているのは、いくつもの論理回路です。では、この回路がきちんと動作するかどうかを確かめるにはどうしたらいいのでしょうか。

　このような問題は故障検出と呼ばれますが、アイデアはシンプルで、ある入力を入れたときに正常な回路とは異なる値を出力した回路は故障しているものとすればいいのです。

　ただし、これは簡単ではありません。入力した値によっては、故障回路がたまたま正常な回路と同じ出力をしてしまう、というようなケースも考えられます（コラム参照）。

　そこで「いくつかのテスト入力を入れて、そのすべてに対して正常な回路と同じ値が出れば故障していない」と考えるようにします。

　では、故障を検出するためのテスト入力はどのように作ればいいのでしょうか。一つ一つ数学的に構築していく方法もありますが、人手と時間が非常にかかります。コンピュータを用いたとしても、大きな回路では可能性のある故障の数が膨大になり、各々の故障を検出するテスト入力を1つずつ作っていくのはたいへん難しくなります。そこで、数学的なアイデアとコンピュータの計算力を上手く使って、最適なテスト入力を作りだす必要が出てきます。これがテスト生成と呼ばれる分野です。

壊れた回路を見つけ出せ

　回路の中には、複数の信号線が入っています。ここでは、全部で3万の信号線が入っているとしましょう。また、このうち100本の信号線が外部からの入力信号線とします。一つの信号線は0か1、どちらかの値をとれます。

　故障を検出するには、まずどのような故障が起きているのかを予め仮定しなければいけません。そこで一般的には、「入力の値によらず、信号線の値が常に0かもしくは1のどちらかに固定してしまう」という故障を仮定します。信号線がグラウンド（アース）に接触してショートしていれば常に0、電源電圧と接触していれば常に1になります。

　また、一つの回路には高々1個しか故障が起きていないということも仮定します。実用上は1つの故障を発見できれば十分なケースが大半だからです。

　この仮定の下で、回路に3万の信号線が入っているとすれば、それぞれが0に固定するか1に固定するか2つの故障が考えられますので、全部で6万通りの故障回路を想定することができます。故障検出のアイデアは、この6万個の故障回路と正常な回路を並列に並べて、すべてに同じ外部入力を与え、正常な回路と異なる値が出たものは排除します。

　このとき、0000…から1111…まで、すべての外部入力を入れて確かめようとすると、2の100乗（約10の30乗）という膨大な値になってしまいますが、最初のうちはランダムな入力を入れても十分に多くの故障を検出することができますので、これを1000回など適当な回数行います。それによって検出できた故障を取り除いた上で、なお残ったものに対してどのような入力なら検出できるのかそれぞれ数学的に求めることで、最終的にあらゆる故障を発見できるようなテスト入力を手に入れることができます。

　複数台のコンピュータを相互補完的に動かす並列計算などを適用することで、このようなテスト生成はより高速に行うことができます。

ハードウェアの設計検証

　設計検証とは、あるハードウェアが正しく設計できているかどうかを確かめるものですが、故障検出と違うのは「正解」となる回路図が存在しないということです。設計した回路図そのもののミスを見つけなければいけません。ここでモデルとなるのは、ハードウェアの仕様書です。仕様書とは「どんなハードウェアを作りたいのか」が書かれたもので、ある入力を入れたときにどのような出力がなされるのかなど、ハードウェアが満たすべき条件がすべてまとめられています。ハードウェアの回路は、この仕様を満たすように設計されます。

　この仕様書が絶対正しいと仮定すれば、ハードウェアがその仕様を満たしているかは数学的に検証できます。このように、論理的な制約条件をシステムが満たしているのかをコンピュータによって判断させる方法をモデル検査と呼びます。

　私たちの身の回りにある信号機の設計で例えてみましょう。

　信号機の仕様書を見たときに、交差点のどちらの方向でも信号機が同時に青になるようなケースがありえた場合、これは危険なので取り除かなければいけません。両方が赤になるパターンは、それに比べれば危険性は低いかもしれませんが、やはりなくさなければいけないミスです。

　これだけ聞くと簡単なように思えますが、最近の信号機はお互いに情報を交換して上手く制御しあうなど複雑に設定されています。そのようになってくると、人間の手だけでは検証が困難になります。複雑で大きなシステムに対して、モデル検査は有効なアプローチです。

ソフトウェアの設計検証

　ここまではハードウェアについて話をしてきましたが、最後にソフトウェアの検証についてもお話しましょう。プログラムが正確に動くかどうかという検証は、ハードウェアの検証よりもさらに難しくなります。ハードウェアは有限の論理回路からできていますので、とることのできる状態数も有限ですが、CやJAVAなどのプログラム言語では、再帰呼び出しといって、何かの手続きAをプログラム中で行うときに、その手続きの中で再び手続きAを呼び出すような操作が可能になっています。この再帰呼び出しを行うと、無限の操作を仮定することができます。つまり、とりえる状態数が無限になりえるのです。無限の状態は、モデル検査のようなアプローチではそのまま扱うことができません。

　コンピュータの中では、データは一時的に「スタック」や「キュー」と呼ばれる構造に格納されます。通常、スタックは十分に大きなサイズなので、オーバーフロー（データが収まりきらなくなって溢れだしてしまうこと）は起こらないと言われます。ところが、再帰呼び出しによって無限の操作が行われると、スタックがオーバーフローしてしまうことがあります。このオーバーフローは致命的なエラーを引き起こす可能性があり、プログラムを作る際には気をつけなくてはいけません。

　これに対処する際には、再帰呼び出しがある部分を別の形で書きなおして有限の範囲で扱えるようにするか、仮にスタックのオーバーフローが起きたときにどうするかという処理を書き足すか、二つの方法が考えられます。今はこのどちらの手法が良いのかを試しているところです。

　プログラムが仕様を満たしているかを判断するモデル検査のような方法がソフトウェアでも使えるようになれば、プログラム検証の敷居はとても低くなります。無限の問題を上手くクリアできれば、人間が一から数学的に検証するよりも、コンピュータに判断させたほうが最終的には早くなるでしょう。

　どのようにしたら、より良い検証ができるのか。便利で効率的な検証を目指して、私たちは日々研究を行っています。

コンピュータの論理回路

　コンピュータの中では、情報はすべて0と1に変換されています。そしてこの0と1をあるルールに従って操作するのが「論理回路」と呼ばれるもので、すべてのコンピュータの基盤となっています。

　たとえば、2入力のAND回路と呼ばれるものは、2つの入力を次のようなルールに従って1つの出力に変換します。

　入力が共に1のときにだけ1を出力し、それ以外のときは0を出力する回路です

　ここで、入力Aの信号線が壊れてしまい、常に0を出力すると、どうなるでしょうか。

　このように、何を入力しても0が出てきてしまうことになります。この故障を発見するには、AとBの両方に1を入れてやればいいことになります。正常な回路ならば1を、故障回路は0を出力し、結果が異なるのですぐに分かります。

　ところが、それ以外の組み合わせを入力しても、正常な回路と故障回路はまったく同じ出力をしてしまいます。これが、「1回の入力だけでは必ずしも故障を発見できない」理由なのです。

アドバイス

　自分で興味を持ち、誰かに教えてもらうのではなく自ら考えて答えを見つけていこうという意欲を持ってください。プログラミングをやっていると、おかしな結果が出たときに、「なぜか」ではなく「どうしたらいいのか」を直接求めたがる人が多くいます。

　やりたいことがあるときに、それには何が必要なのかを考えていく。WEBで調べてすぐに答えを求めたり、あるいは答えをそのまま覚えようとするのはやめましょう。

　「なぜそうなるのか」という仕組み、結果に至るための考え方を理解すれば、結果的に覚えることは少なくなります。ぜひ、自分の頭で考える習慣をつけてください。