写真●Clarke氏らが執筆したモデル検査の教科書
写真●Clarke氏らが執筆したモデル検査の教科書
 ACM(Association for Computing Machinery)は,2007年のチューリング賞(A. M. Turing Award)を,モデル検査(model checking)技術の開発者・研究者で同技術の草分けである3人,Edmund M. Clarke氏,E. Allen Emerson氏,Joseph Sifakis氏に授与することを決定した。賞金として25万米ドルが,米Intel Corp.および米Google, Inc.より贈られる。授賞式は2008年6月に米国サンフランシスコで開催される予定である。

 チューリング賞はコンピュータ分野の「ノーベル賞」といわれるほど名誉ある賞であり,英国のコンピュータ科学者のA. M. Turing氏にちなんでいる。過去に,セマフォの考案者のE. W. Dijkstra氏(1972年),並行システムの記述言語のCSPやホーア論理の考案者のC. Antony R. Hoare氏(1980年),最近では「人月の神話」などの著書で有名な「S/360」開発者のFrederick P. Brooks氏(1999年),Smalltalkやパソコンの父として有名なAlan Kay氏(2003年),TCP/IPの父といわれるVinton G. Cerf氏およびRobert E. Kahn氏(2004年)など,コンピュータ分野の名だたる巨人達が受賞している。前回までは,賞金はIntel社のみの提供で10万米ドルだったが,今回からGoogle社が加わり賞金が増えたようだ。

LSIの回路設計検証などに貢献

 今回の受賞対象になったモデル検査は,LSIの論理回路設計やソフトウエアの状態遷移モデルの検証に用いる技術である。並行システムを特定の記述言語で記述し,それが所定の性質を満たすかどうかを,コンピュータ上でしらみつぶしに探索する。検証項目は,「時相論理(temporal logic)」と呼ぶ,時系列でのイベントの成立状況を表現できる特殊な論理式で記述する。与えた時相論理式を満たさない状態遷移パスが見つかった場合,それを反例(counter examples)として出力する。

 モデル検査は,基本的にはしらみつぶしに状態空間を探索するため,状態遷移の組み合わせが膨大になる「状態爆発」と呼ぶ問題がある。状態空間の表現をいかに抽象化したり,探索空間を合理的に枝刈りしたりするかが,実問題への適用において課題となる。さまざまな工夫が提案されてきており,中でも今回のClarke氏とEmerson氏は「シンボリック・モデル検査(symbolic model checking:SMV)」と呼ぶアルゴリズムを考案したことで知られる(Sifakis氏は,Clarke氏らとは独立に研究)。モデル検査のアイデアは古く1970年代に生まれたが,Clarke氏らはこのSMVの理論を1981年に発表し,その後,LSIの論理回路の検証用途などに実用化の道を切り開いた。

 「シンボリック」というと,通常,変数への置き換えを想像するが,SMVでは論理式そのものを1つのシンボルに置き換えることで,探索を効率化する。状態空間は「BDD(binary decision diagram)」で記述する。同名の「SMV」と呼ぶツールがあり,現在は「NuSMV」と呼ぶ新版の検証ツールが広く使われている。

 モデル検査は,当初,マイクロプロセサの制御回路や演算器などLSIの回路設計検証で花開いた。チューリング賞の賞金スポンサーとなっているIntel社などは,まさにモデル検査技術の「大口ユーザー」であり,実際,Clarke氏らと活発に協業していたようだ(LSI設計分野では,モデル検査というよりも,「フォーマル・ベリフィケーション(formal verification)」という名称で知られている)。

ソフトウエア分野での評価はこれからか…

 その後,状態空間の探索の効率化手法として「有界モデル検査(BMC:bounded model checking)」と呼ぶアルゴリズムが登場する。これにより2000年代になってモデル検査はソフトウエアの振る舞いの検証用途としても大きく注目を浴びるようになった。BMCは,SMVやSPINに代表されるそれまでのモデル検査技術と異なり,探索を一定の深さで打ち切る。このため網羅的な検証は期待できないものの,設計に潜むバグを手早く見つける用途では有効に働くのだ。

 最近では,自動車分野などで「機能安全(functional safety)」と呼ぶ安全規格の策定が進んでおり,その中でモデル検査による検証などが推奨される見込みである。こうした国際規格の影響もあり,ここ数年,日本でも自動車の組み込みソフトウエアなどを中心に,モデル検査は高い注目を集めるようになった。

 ただし,今回のチューリング賞の対象になった業績は,モデル検査の技術の歴史でいうと比較的初期の業績に当たる。ソフトウエア分野でのモデル検査の注目の高まりも受賞に影響しているのかもしれないが,ACM会長のStuart Feldman氏が授与に当たって「Clarke氏らの業績は,半導体業界に多大なインパクトを与えた」とコメントしているように,既に多くの実績がある,LSIの設計検証での貢献が評価ポイントになったといえそうだ。

 ちなみに,1980年のチューリング賞受賞者のHoare氏は,現在,Microsoft Researchに籍を置いており,モデル検査に代表される形式検証の技術を発展させ,プログラムを対象とした検証を可能とするべく「The Verifying Compiler」と呼ぶプロジェクトを推進している。米Microsoft Corp.は,モデル検査の研究・実用化でも秀でており,実際,Windowsのデバイス・ドライバの検証ツール「SDV(static driver verifier)」には,Microsoft Researchの研究者が開発した「SLAM」と呼ぶモデル検査技術が使われている。

<日経エレクトロニクス関連記事>
ソフトウエアは硬い
モデル検査でバグ発見 富士ゼロックスがMDDで
Cプログラムの検証をモデル検査で,NECや松下が相次ぎ技術開発
レクサスのカイゼン

<ソフトウエア分野でのTech-On!関連記事>
【JaSST】富士ゼロックス,MDDへのモデル検査の適用事例を発表
アルゴ21が形式手法に注力,車載ソフトに向けCSPの教育を15名の技術者に
モデル・ベース開発で形式検証,自動車業界で実績上げるドイツOSC ES社の検証ツール
PolySpace社を買収し検証技術に注力するMathWorks社

<LSI/EDA分野でのTech-On!関連記事>
「フォーマル・べリファイア」とは(EDA用語事典)
「サクッと書いてサクッと検証」,富士通九州が米Cadenceの形式検証を評価
【ASP-DAC 2006】検証危機には「方法論の徹底」が効く
検証クライシスに対する米Intelの提言:ASP-DAC技術講演から
「検証漏れは許さない」,独OneSpin社が説くRTL検証手法