設計の正しさを確かめる論理の力 —速く確実に設計ミスを見つけ出すために—

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

速く確実に設計ミスを見つけ出すために

 現在、私たちの生活や社会の重要な部分で、大規模なシステムがたくさん稼動しています。社会のインフラを支えるような大きなシステムは設計も大掛かりとなり、設計に誤りがないかを調べる「設計検証」も当然複雑なものとなります。また、生活に密接に結びつくシステムでは、たったひとつの設計ミスがあってももたらされる損失が大きく、設計ミスを見落とし無く確実に見つけることも課題となっています。平石裕実先生は、時相論理を用いて設計を検証する方法の研究がご専門です。論理で設計を検証するとはいったいどのような方法なのかをお話しいただきました。

ますます困難になる設計検証

  コンピュータの登場により、私たちの周りで働く機械や装置などのシステムが複雑化・大規模化してきました。近年のコンピュータの計算能力の向上が、この傾向をますます強めています。様々な装置が自律的に動くことで、私たちの生活は便利になったりコストが低くなったりとメリットもたくさんありますが、それと同時にシステムの設計に間違いがないかを検証することもより難しくなっています

 また、金融や社会インフラなど、経済活動や日常生活になくてはならないところでコンピュータシステムが使われています。これらのシステムは、一般に規模が大きいだけでなく、絶対に設計ミスがあってはいけないという点が特徴です。銀行のオンラインシステムに不具合があれば、多くの人に影響が出て、お金の損失も出るでしょう。発電所のシステムが止まってしまえば、最悪の場合、命にかかわる事故につながるかもしれません。

 大規模で複雑なシステムやわずかな設計ミスも許されないシステムは今後ますます増えていくと考えられます。この現状に対して従来の設計検証の方法では限界が現れてきました。いくつかの例を挙げてみましょう。

 1993年にインテルが製造したあるプロセッサは、特定の数値の割り算で誤った答えを出しました。割り算の計算を高速にするため、あらかじめいくつかの割り算の答えを表にしておいて、その組合せから答えを出すという仕組みを用いたのですが、その表を作成する際に設計ミスが起こったのです。多くのユーザが交換を希望したため、莫大な損失(約4億7500万ドル)となりました。

 1996年には、EUのロケット、アリアン5が打上げ後約40秒で爆発する事故が起きました。ロケットの推進能力が一世代前のアリアン4から大幅に強化されたため、姿勢を制御するプログラムが扱える数値の範囲を超えてしまったからでした。設計ミスとしては史上最も高くついた事例と言われています。

従来の設計検証の限界

 それでは、従来の検証方法のどこに限界があるのでしょうか。従来の検証方法のひとつに論理シミュレーションと呼ばれるものがあります。ユーザがどのような使い方をするのかを想定して、その場合の結果を調べる方法です。設計者は様々な使い方を想定してシミュレーションを行いますが、先述したインテルのプロセッサの場合、間違った答になるのは2万7千年に1回の頻度で行われる計算だったと言われています。アリアン5の場合は、アリアン4までは問題のなかったプログラムを再利用しましたが、アリアン4では想定されていなかった大きな加速度が加わり、その計算が正しく行われなかったのです。いずれの場合も設計者が想定していない計算が現実に行われてしまったのです。

論理シミュレーションによる設計検証

 論理シミュレーションによる設計検証の方法を、非常にシンプルな例で見てみましょう。設計するのは、100円の商品を売る自動販売機で、投入できるコインは50円と100円です。100円で商品1つ、100円を超えると商品1つとお釣(50円)を返します。

 下図がこの自動販売機の設計図です。スタート直後はAの状態になり、矢印が状態の遷移(移り変わり)を表しています。矢印(遷移枝)に書かれているのは、利用者の行動と自動販売機の出力です。「100円/商品」は「利用者が100円を入れる/自動販売機が商品を出す」という意味です。

 さて、自動販売機を作動させると、状態Aからスタートします。状態Aで100円を入れると商品を出し、再び状態Aへと戻ってきます。状態Aで50円を入れると何もせずに状態Bへと移ります。

 シミュレーションにより設計を検証するには、利用者の使い方を想定し、自動販売機の状態遷移を調べます。たとえば次のような状態遷移を想定すると

A→50円/何もしない→B…問題なし
A→100円/商品→A…問題なし
A→50円/何もしない→B→50円/商品→A…問題なし
A→50円/何もしない→B→100円/商品+お釣→C…問題なし
A→50円/何もしない→B→100円/商品+お釣→C→50円/何もしない→D…問題なし

 ここまででは設計ミスが無いように見えます。では、50円、100円、50円、100円、50円と入れるとどうなるでしょう?

A→50円/何もしない→B→100円/商品+お釣→C→50円/何もしない→D→100円/商品+お釣→D→50円/商品→C

 合計350円入れたのに対して、商品が3つとお釣が2回出てきました。つまり350円で400円分出てきたことになります。ここではじめて設計ミスがあると分かりました。この自動販売機は50円と100円しか使えないうえに商品も1種類だけという非常にシンプルなものですが、それでも最初の5通りのシミュレーションではミスが現れませんでした。実際のシステムはこれとは比較にならないほど複雑なものなのです。

 現実の複雑なシステムでは、設計が正しいと言うために何通りのシミュレーションをすればいいのか、確実な正解はありません。100万通りのシミュレーションをパスしても、100万1通り目で不具合が生じるかもしれないからです。加えて、実際に運用されるシステムの状態数は100万をはるかに超える場合が一般的なのです。

数学的に設計の正しさを証明する

 このような設計検証の難問に対して、ひとつの光明が現れたのは1980年代後半のことでした。システムの設計の正しさを数学的に証明する形式的設計検証の画期的な方法が提案されたのです。

 それは、システムの状態や遷移を集合としてまとめて、集合を論理関数(※次章にて詳しく説明)によって表現する「記号モデル検査」と呼ばれる方法です。記号モデル検査では、状態を変数とした論理関数を作り、それを満たす解があるかないかを計算することで、設計を検証することができます。

論理関数を使った設計検証


 高校生のみなさんには、論理関数という言葉はあまり聞き慣れないかもしれません。ここでは論理関数による表現とその操作について触れておきましょう。

 論理関数とは、論理式で表された関数のことです。論理式には、通常の四則演算とは異なる論理演算が適用されます。主な論理演算には「論理和(or)」「論理積(and)」「論理否定(not)」などがあり、それぞれ「和集合」「共通集合」「補集合」に対応します。1(真、ある)と0(偽、ない)の二進法で表されます(表1)。

 先ほどの自動販売機の例で実際の論理関数による設計検証を見てみましょう。変数xとyとを使い状態A、B、C、Dをそれぞれ(x,y)=(0,0)、(0,1)、(1,0)、(1,1)とし、変数zを使って50円を0、100円を1とすると、表2のように各遷移枝を(x,y,z)で表すことができます。

 このとき、次のようにそれぞれの集合を表せます。

 商品を出した直後の状態集合X={A,C,D}

 集合Xから出ている50円の遷移枝の集合Y={a,e,g}

 商品を出す遷移枝の集合Z={b,c,d,f,g,h}

 いずれの論理関数も集合を現した式です。各遷移枝のx,y,zの値を代入して、1となる枝は集合に含まれ、0となる枝は含まれません。

 ここで、集合Y(商品を出した直後に50円入れた)と集合Z(商品を出す)の共通部分Y∩Zを論理演算したとき、必ず0にならなければ正しい設計ではありません。Y∩Zは「商品を出した直後に50円入れると商品が出てくる」を意味するからです。

 ところが、この設計ではY∩Z=1を満たす遷移枝が存在します。g(1,1,0)です。確かめてみましょう。

 確かにgはY∩Zに含まれています。よって、この設計はgの部分に誤りがあると分かるのです。

 記号モデル検査のメリットは、シミュレーションのように「どこまで確かめれば正しいと言えるのか」という問題がなく、論理関数を満たすか満たさないかという数学の問題に置き換えることで明確な解答が得られることです。さらに、状態や遷移枝を集合として扱うことで従来よりもずっと大きなシステムを検証することもできるのです。変数が1000個ぐらいまでの論理関数の計算は、現在のコンピュータでも十分可能な範囲です。0,1の2通りが1000個ですから、21000≒10300程度の状態や遷移枝を計算することができるのです。この計算能力は年々向上していて、今後さらに大きな論理関数も扱えるようになっていくでしょう。

数学が支える安心できる社会

 現在、数学的に設計を検証する方法は、コンピュータ関連の企業を中心に実際に使われはじめています。先に登場したインテルをはじめマイクロソフトなどでも実用化や研究が進められていて、今後ますます必要とされるものになっていくと考えられます。当然、数学的な設計検証ができる人材もより求められるようになるでしょう。検証ソフトそのものや、ハードウェア・ソフトウェア・システムの記述言語との連携も大きな研究テーマになっています。

 設計ミスを事前にすべてなくすことができれば、安全性と信頼性を確保できるだけではなく、より大規模なシステムを作成するなど私たちの創造性をもっと活かせる社会になることでしょう。それを実現するのが数学の論理の力なのです。

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

プロフィール

工学博士。専門は論理システムの設計検証。設計検証の速度を向上させるための並列コンピューティング(特にマルチプロセッサ※1)も研究対象。研究室にはプログラムを学ぶ学生も多く、設計検証ソフトのユーザ・インタフェースの改良も研究テーマのひとつ。高校生へのアドバイスをたずねると「一口に数学と言っても、連続的なもの(微積分など)と離散系のもの(組合せなど)とに分かれ、得意分野も人によって分かれる。微積分が苦手でもあきらめずに、論理的に考える習慣を身につけて、きちんと証明するトレーニングを積んでほしい」とのこと。
※1 複数のCPUを使って計算を行うこと。一般に単体のCPUよりも計算能力が高まる。

PAGE TOP