1.はじめに

　現在、多くの電子機器は、ハードウェアとソフトウェアを組み合わせたシステムとして設計されている。これらのシステムの設計は、半導体微細化技術の進歩と要求される仕様の高度化により、急速に複雑さが増している。一方で、集積度向上の伸びに比べて設計生産性の伸びは低く、その差が広がっており、計算機による設計支援が重要になっている。集積度向上の結果、一つのシリコンチップ上にシステム全体を集積するシステムオンチップ(System-on-a-Chip)が実現されている。このような大規模システムでは、システム全体の実行プロセスは、いくつかの並列に動作する実行プロセスの集まりとして成り立っている。そのため、1つのプロセスに注目するだけでは、システム全体の動作を把握することが困難である。このような並列プロセスを設計者の意図通り実行させるためには、プロセス間の実行順序のスケジューリング(同期)が不可欠である。

　本論文では、システムレベル設計で用いられるCベース設計言語の1つである、SpecC言語におけるモデル検査法に基づく同期検証を提案する。検証するモデルの規模を小さくするために、提案手法では述語抽象化法を利用している。提案手法では、SpecCプログラム中でデッドロックが起こりうるかどうか、つまり、あるプロセスの実行が停止したままになりうるかどうかを形式的に検証することができる。述語抽象化を施した抽象モデルにおいてデッドロックが起こらないことが証明された場合には、元のSpecCプログラムでもデッドロックが起こることはない。しかし、モデル検査の結果として反例(デッドロックを起こす実行シーケンス)が得られた場合には、その反例を解析し、元のSpecCプログラム中で反例に対応する実行シーケンスが存在しない場合には、抽象モデルを改良し、さらに検証を続ける必要がある。また、反例に対応する実行シーケンスが元のプログラム中に存在する場合には、デッドロックが起こりうるという結果を得る。なお、提案する手法は完全に自動化することが可能である。

2.モデル検査法における抽象化技術

　モデル検査法は、分かりやすく、完全に自動化が可能な手法であるため、広く用いられている検証手法である。モデル検査法では、有限状態から成る並行動作システムにおいて、あるプロパティ(仕様)が成り立つかどうかを証明することができる。しかし、この手法では、状態数が膨大になってしまうと検証が現実的な時間では終了しないという問題点があり、これを解決するために、検証するモデルの状態数を減らす多くの手法が提案されている。その中でも、抽象化は非常に有用な手法である。抽象化とは、具体モデルからより状態数の少ない抽象モデルを導出する手法である。そのため、抽象モデルでは高速にモデル検査法によって検証を行うことができる。しかし、抽象モデルでは、具体モデルでは存在しない実行シーケンスが生じる場合がある。そのため、抽象モデルで証明されたプロパティは具体モデルでも成り立つが、抽象モデルで証明できなかったプロパティであっても具体モデルでは成り立つ可能性がある。

　モデル検査器があるプロパティの検証に失敗した場合には、反例が作られる。しかし、抽象化が適用されていると、この反例がfalse negativeである可能性がある。そのため、この反例を解析し、その結果false negativeである場合には、この反例が存在しなくなるように抽象モデルを改良する必要がある。

3.SpecC言語における同期

　SpecC言語は、仕様設計からRTL(register transfer level)に至るシステム全体を記述するためのシステム設計言語である。そのため、ハードウェアとソフトウェアをシームレスに記述することができるという性質を持つ。SpecC言語では、par 文を用いて並列プロセスを記述することができる。例えば、図1のようにpar{a.main(); b.main()}と記述すれば、behavior aと behavior bが並列に動作することになる。それぞれのbehavior内では、各文はC言語のように順次実行される。その結果、behavior aにおけるタイミング制約は、

Tas≦T1s＜T1e≦T2s＜T2e≦Tae

となる。なお、T1、T2は図中の文st1、st2に対応するタイミングであり、添え字，eは実行の開始と終了に対応する。この段階では、各文の実行順序はst1→st2→st3，st3→st1→st2，st1→st3→st2のいずれであるか決定することはできない。この場合、意図しない結果や同じ変数xへの同時アクセスが起こり得る。この問題に対応するため、SpecC言語ではイベント受け渡しによる同期の構文(notify/wait)が提供されている。waitが実行されると、対応するイベントを引数とするnotifyが実行されるまで、wait側の実行が停止する。図2では、図1のプログラムにwait/notifyを挿入することによって同期を実現している。その結果、st3がst2の後に実行されることが保証される。

4. 同期検証

　ここでの同期検証の目的は、与えられた並列実行を含むSpecCプログラムが正しく同期されているかどうかを検証することである。SpecCプログラムの抽象化手法として、ブールプログラムの概念を応用している。検証の流れを図3に示す。この検証全体は、完全に自動化することが可能である。以下では、検証の各ステップを簡単に述べる。

1.与えられたSpecCプログラムを抽象化し、boolean SpecCを導く。この抽象化では、

・イベントに関する文(wait/notify)はそのまま残す

・条件分岐の条件を表す式は互いに独立な新たな変数によって置き換える(例えば、if(x>0)はif(C0)で、if(y<3)はif(C1)で置き換えられる)

・その他の全ての文は、何も実行を行わないskip文と置き換えられる

2.boolean SpecCからTas≦T1s<...のような各文の実行のタイミング制約を表す数学モデルを導く

3.モデル検査法に基づいてタイミング制約を表したモデルを検証する。ここでは、Difference Decision Diagram(DDD)を用いて検証を行う。DDDは、decision diagramの一種であり、等号・不等号で表される条件式を効率的に表現できるという特長を持つ。モデル検査のプロパティとしては、「デッドロックが起こらない」ことを与える。モデル検証の結果は、

・デッドロックは起こりえない(この場合、「検証成功」となり終了する)

・デッドロックが起こりえる(この場合、反例もともに出力される)

のどちらかとなる。

4.Cooperating Validity Checker(CVC)のような式の成否を判定するツールによって、得られた反例が元のプログラム中でありえるかどうかを解析する。反例が元のプログラムではありえないシーケンスであることが証明されれば、次の改良の段階へと進む。そうでない場合には、「検証失敗」として、元のSpecCプログラムでの反例を出力して、検証を終了する。

5.抽象モデルでの反例が、元のプログラム中で対応するシーケンスが存在しない場合、過度の抽象化を行っていることが原因である。そのため、この「偽の」反例を作る原因となっている条件変数を特定して改良を行い、新たな boolean SpecCプログラムを導き、検証を繰り返す。

6. 結論

　本論文では、SpecC言語で記述されたシステムの同期検証の手法を提案した。提案手法は、SpecCプログラムの抽象化と反例に基づいた抽象モデルの改良に基づいたものである。ブールプログラムの概念を取り入れることによって、同期に関係するwait/notify文と条件分岐に関する条件文以外の全ての部分を抽象化し、高速なモデル検査を実現した。モデル検査では、デッドロックに関するプロパティを与えて検証を行うが、検証に失敗した場合には、デッドロックが起こるような抽象モデル上での反例が返される。そこで、その反例の解析を行い、もし元のプログラムでは存在しない反例である場合には、この「偽の」反例が生じる原因となっている条件式を特定し、抽象モデルを改良する手法を示した。

　システム設計において、同期検証は最も重要な検証事項の一つである。提案手法は、同期に関する部分のみを残す抽象化手法を適用することにより、同期検証に特化した、大規模設計記述に対応可能な検証手法となっている。

図1:behavior aとbehavior bの実行タイミングダイアグラム

図2：図1のプログラムに対する同期(notify/wait)の導入

図3:提案する同期検証手法

　本論文は、「Formal Verification of Synchronization in System-Level Design」(システムレベル設計における形式的同期検証に関する研究)と題し、デジタル電子機器設計の上位設計段階であるシステムレベル設計において、その正しさを数学的に証明する手法である形式的検証手法、特に、複数の並列動作するプロセスの同期に関する検証技術について研究したもので7章より構成されている。

　第1章は Introduction(序論)であり、研究の背景と目的を述べている。システムLSIに代表されるように近年のデジタル機器設計は、大規模・複雑化しており、設計期間の長期化が大きな問題となっている。特に、設計の正しさの確認作業である設計検証に要する期間が相対的に長くなっており、特に大規模設計の場合、全体の設計期間に占める設計検証期間の割合が80％を超えるほどになっている。本論文では、その現状を分析し、従来のシミュレーションやエミュレーションだけでなく、設計の正しさを数学的に証明する形式的手法の必要性・有用性、特に、大規模・複雑な設計に対応するために、システムレベル設計と呼ばれる設計の初期段階での形式的検証の重要性を述べている。次に、従来の形式的検証技術のサーベイを簡単に行い、システムレベル設計における検証問題として、複数のプロセスが互いに同期しながら、正しく作業を進めることを検証する「同期検証」の重要性を説明し、システム設計における同期検証を形式的に行うフレームワークの構築と、それの上での効率的な形式的検証手法を本論文の目的としていることを述べている。

　第2章はPreliminaries and Backgrounds(準備と背景)であり、本論文で使用する既存技術の説明を行っている。まず、デジタル機器設計におけるシステム設計とは何かについて説明し、システム設計記述に利用するSpecC言語の要点を簡単に紹介している。本論文では、SpecC言語で記述されたシステム設計記述に対して、形式的に検証を行う。さらに、本論文で利用する形式的検証技術に関する既存技術の説明を行っている。

　第3章はSynchronization Verification(同期検証)であり、本論文が提案するシステム設計に対する同期検証手法を説明している。本論文で提案している同期検証のフレームワークでは、与えられた検証すべきシステム設計記述に対し、まず設計の抽象化を自動的に行う。この抽象化により大規模設計に対しても適用可能な検証手法となっている。次にその抽象化された設計記述に対して、複数の並列動作するプロセスが正しく時間軸上で同期しているかを調べるために、時間関数の式に展開し、それを解析する作業をモデルチェッキングと呼ばれる形式的検証手法を用いて行う。この解析に矛盾がなければ元の設計は正しいと言える。一方、設計に誤りがある場合には、解析の結果、反例が検出される。この反例は、抽象化された設計に対するものであるため、抽象化によっては、元の設計では成り立たない反例である場合がある。このため、検出された反例を元の設計で確かめる作業を行う。もし、元の設計でも反例となっている場合には、設計誤りが見つかったことになる。しかし、元の設計では反例となっていない場合には、検証のために行った設計の抽象化に問題がある(抽象化しすぎている)ので、抽象化処理の改良を行う。以下、これらの作業を元の設計に対する反例が検出されるか、または、設計が正しいと証明されるまで、繰り返していく。本章では、この検証フレームワーク全体の処理の流れの説明を例題も利用して詳しく行っている。システムレベル設計の同期検証に対するこのような形式的検証のフレームワークは本論文によって、新規に提案されたものである。

　第4章はAbstraction and Model Checking(設計の抽象化とモデルチェッキング)であり、3章で説明された検証フレームワークにおける、設計の抽象化と抽象化された設計のモデルチェッキング手法による解析に関し、そのアルゴリズムについて例題を使いながら、詳細に説明している。設計の抽象化では、設計記述の同期に関する部分以外を取り除く処理を行っており、元の設計が大規模な場合でも、大幅に設計規模を縮小できる。また、それに続くモデルチェッキングによる解析では、時間関数による条件式の形で定式化するという新しいアルゴリズムを提案しており、実時間処理に関する記述を含む設計記述の検証が可能となっている。このように、大規模・複雑な設計に適応可能な新規アルゴリズムが提案されている。

　第5章はAbstraction Refinement(設計抽象化の改良)であり、4章で行った設計抽象化が、誤って反例を提示してしまう場合に、その誤りの反例を提示しないように設計の抽象化を自動的に改良する手法について、検討し、新規手法を提案している。問題の性質上、発見的手法となっているが、後の実験結果が示すように、効率的に作用する場合の多い手法が提案されている。

　第6章はImplementation and Experimental Results(実装と実験結果)であり、3章、4章、5章で提案している同期検証のフレームワークの実装法の検討と実装結果の説明、それに、数種の例題に対して、実際に同期検証を行った結果について報告している。実装は、設計の抽象化とそのモデルチェッキングによる解析(4章で説明した部分)については、自動化が実現されている。また、設計の抽象化の改良については、効率的に検証を行うために一部対話的に処理する形でツールとして実現されている。実際に制御システムや通信プロトコルの検証に適用した結果、元の設計に対し、抽象化された設計が極めて小さくなることが示されており、本論文で提案する同期検証のフレームワークは十分実用的価値があることが、実験的に証明されている。

　最後の第7章は、結論であり、本論文の研究成果をまとめるとともに、今後の方向について議論している。

　以上、本論文は、大規模デジタル電子機器のシステム設計において、もっとも設計誤りを生じやすい並列プロセス間の同期に関し、大規模設計にも適用可能な検証フレームワークを提案、実装し、例題で評価することでその有効性を示したもので電子工学の発展に貢献するところが少なくない。

　よって、本論文は博士(工学)の学位請求論文として合格と認められる。