1. HOME
2. 研究・社会連携
3. 産官学連携
4. 研究探訪（研究者紹介）〜サギタリウスからのメッセージ〜
5. コンピュータ理工学部ネットワークメディア学科 平石 裕実 教授

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

これまでのシミュレーションによる検証手法の課題をクリア。ハードウェア＆ソフトウェアの設計の正誤を自動的にチェックする画期的な形式的検証システム

現在、取り組んでおられる研究開発の内容について教えていただけますか。

　大規模なハードウェアや複雑なソフトウェアの設計に誤りがないかどうかを、数学的な手法を駆使して自動的に証明する形式的論理設計検証が研究テーマです。これまでの設計検証手法は設計したシステムの動作をコンピュータでシミュレート（模倣）する方法が中心ですが、これではすべての動作パターンを検証することができませんので、設計ミスを見落とす危険性があるわけです。
　一般的に設計者には設計に自信のあるところと少し不安の残る箇所があり、結果的に気になる部分を中心にシミュレートすることになります。しかし、人間が行うことですから想定漏れも生じます。仮想的な入力を上手く与えるのがむずかしいケースもあります。
　また、あまりにも多いと時間的にすべてをチェックするのが不可能な場合もあるわけです。 　具体的な事例では、たとえば米国北東部で発生した大停電。当然、バックアップシステムが組み込まれているわけですが、故障したケースでどのように作動するかを事前に検証するのはなかなか難しいのです。また、通常、故障は一カ所の想定でシミュレートしますが、実際には稀に同時多発することもあります。さらに、実績があり信頼できる設計はあらためて設計し直すことによって生じるミスを防ぐために、新たなものと組み合わせて用いますが、環境が変わることで変調をきたすこともあります。さらに、携帯電話のように新製品の競合が激しいものは、検証にかけることのできる時間が限られています。これらをクリアするために、設計の正しさを数学的に証明する形式的検証手法の重要性が増してきているのです。

研究を開始されたのはいつ頃ですか。産学連携の状況についてもお聞かせください。

　研究をはじめたのは1980年代の中頃です。 当初は理論的には興味深いが、実用化までにはかなりの歳月が必要だと言われていました。 検証関係の研究者は早い時期から注目していましたが、現場の設計者にはなかなか受け入れてもらえませんでした。それでも、'90年代の半ばには国内外のコンピュータメーカーで、従来の方法と数学的な検証手法をケーススタディで比較評価するようになり、数学的な設計検証を試みた方が好結果が出るという事例が数多く発表されるようになりました。現在は、企業規模にもよりますが、実用レベルで採用する企業が出てきています。設計の初期の段階では従来のコンピュータでシミュレートする方法を行い、最終段階で形式的検証システムを用いて押さえていくという組み合わせ手法を採っているケースが多いようです。また、この論理設計検証を広く普及させるためには敷居を低くする努力も必要だと考えています。
　まだ、現場の設計者の方々には使いづらいところがあるのではと感じます。
　検証をサポートするようなツールやプログラムはあるのですが、実際に用いるとなると最低限理解しておかなければならない数学的な知識が必要です。なぜ、このツールを用いれば検証ができるのかという原理も理解しなければなりません。これがネックになっているように思います。この分野を担う優れた人材を大学で育成することも重要です。これができないと海外への外注が増加し、人的な空洞化が起きてしまう危険性があります。現在、研究においてはパーフェクトな検証を、いかにスピーディに行えるようにするか。これが課題です。個別にチェックしていたのでは非常に時間を要しますので、百万通りあるとすれば、共通性のある十万をまとめてシミュレートするような手法を追求しています。欧米での研究も盛んで、新たな方法が次々に提案され実用化されつつあります。今後、さらに大きく飛躍する分野だと考えています。