=========================================================================== 分科会2 セッションSA-7:「形式的手法を使って楽をする方法」 コーディネータ: 藤倉 俊幸(豆蔵) 席数　　　 : 100人程度 参加人数　 : 30人程度 パネラ(50音順) 　青木 利晃(北陸先端科学技術大学院大学) 　倉岡 幹雄(I-Logix Inc.) 　関本 康久(日本テレロジック) 　佐原 伸　(日本フィッツ株式会社) 　高橋 孝一(産業技術総合研究所) 　水口 大知(産業技術総合研究所) 　向山 輝　(NEC) =========================================================================== 藤倉: 形式的手法は、組込みソフト開発者間でさほど知られていない。 そこで、各パネラに各々の立場から、どんな形で形式手法と関与しているのか紹介 して貰う。 形式的手法が、どんな場面で役に立つか例を挙げる。 ランボー(Rumbaugh)の本「Object-Oriented Modeling and Design」の中にあるATM の例題をモデル検査したところ、デッドロックを検出したのである。 現状の組込み開発においても、実行テスト等をするが、仕様の段階ではそれほど詳 細には行わない。この例には、対応するソースコードはないが仕様だけで誤りを発 見できた。これがシステム設計における形式的手法のメリットである。 実行テストの段階で仕様の間違いを発見することがあるが、仕様の間違いをなんで ソースコードにしなければ分からないのか。 仕様の間違いは仕様の段階で、設計の間違いは設計の段階で発見できるようにする ものが形式的手法である。 佐原:(形式的手法の推進派) 形式手法を用いた証券業務のシステム開発を行っている。組込みとは場違いな事務 処理系の開発であるが、基本は変わらない。 システムの記述、個々の要件はあまり変わらないので、多少は参考になると思う。 形式手法に関して、 例えば、プログラムというのは1つの数学系である。 形式手法というものは、数学をベースに何かものを作るということである。その中 でも、プログラムは検証困難な数学系である。下手に狂ってしまうと、検証ができ ないことが、ほぼ分かっている。だから、どこかで数学的な変更をしなければなら ない。 ところが、現場では何が行われているかというと、プロジェクトの最終工程でよう やく数学的な変換が行われている。でも、検証は困難である。なぜかと言うと、正 しくないものを一旦作ってしまったら、つまり、仕様が間違っている、あるいは設 計が間違っていると、プログラムをいくら頑張っても、必ず間違いが起こってしま う。 それに対して、形式手法だと、上流の仕様から、正しい変換を繰り返すことで、段 階的に洗練させていくので、検証が可能になる。自動的に検証するには、それなり に工夫がいるが、今までより、かなり検証できるようになる。 開発現場の経験から言うと、日本語で正しい仕様を書くことは難しい。例えば、人 や地域によって表現方法が異なる。当然、曖昧さの排除も困難で、再利用などもほ とんどできない。 では、最近流行りのUML ならどうかというと、大規模プロジェクトで実際にやって みると、非常に難しい。できないことはない。日本語でやるよりは多少いい。 UML を用いる場合、まず、仕様記述言語に記述する前に、OCL という制約記述言語 がある。これは、ちゃんとした仕様記述言語ではないので、形式手法でいうところ の仕様はちゃんとは書けない。再利用や、ツールによるチェックがほとんどできな い。 それがなぜかと言うと、UML という言語が意味的にしっかりと定義されていため。 最近のUML2.0では、ほとんど形式仕様より難しいくらいの言語である。要は、形式 手法は難しいかと言うと、確かに難しいが、では、従来技法が易しいかと言うと、 そんなことはなく、むしろ、従来技法の方が難しいし、あるいは、UMLの方が難しい。 実際にやってみると、やはり、従来の方が難しい。2,3年前に証券会社のシステム 130万行くらいの内、8万行くらいのサブシステム2つを私のチームで(形式手法を用 いて)開発したことがある。結果、生産性は見積りに対して、だいたい36〜39%くら いで済んだ。 ただ、他の一部の(形式手法を用いてない)サブシステムでも、これに近い生産性を あげていた。そのため、形式手法を使ってもあまり生産性が上がらないと言われた が、実際にリリースが始まると、リリースされた後のバグの出具合が形式手法を適 用した部分は少なく、15倍以上の信頼性をあげている。 では、開発の進め方は、どうしたのかと言うと、ただ単に形式手法のみを使ったわ けではなく、ソフトウェア工学の当たり前のことは一通りやった。 要求定義は、ユースケースを使った。専門家が作成した。 それから、私ともう1人の専門家がVDM++というオブジェクト指向化した形式仕様記 述言語で仕様を作成した。つまりシステムで何をすべきかを記述した。恐ろしいこ とに、このチームは証券業務システムを開発したものはほとんどいない。 C++とJavaで実際には実装したが、これまでにC++とJavaで業務用アプリケーション を組んだ経験のあるプログラマも1人もいない。にもかかわらず、仕様を作成し、 開発支援ツールを使って仕様レベルで98%のカバレッジにし、仕様として、作ろうと 思ったものは、ほぼ作れているくらいの検証はしている。 それから、プログラミングでは、一応、事務処理系のフレームワークを作成し、そ れを使ってプログラムするという当たり前のことをした。また、管理の方も、ソー スコードは全部 CVSでバージョン管理して、誰がどういう理由で直したか、いつで もトレースできるようにした。リリース後のトラブルは、記録していつでも誰でも 見れるようした。このように、ソフトウェア工学的に使えるものは使って、それに、 この VDM++というものを使って形式手法の仕様を使った。だが、もちろん、形式手 法を全部使ったわけではなく、仕様をちゃんと書くというところに一番重点を置い てやった。 結果、形式手法は使えるのかと言うと、Yes。 実際にNASAや原発や列車の制御など失敗すると人の生死に関わるようなシステムで は使われている。ただし魔法ではない。それなりに苦労しなければならないが、苦 労した分の成果はある。 形式手法は難しいかと言うと、Yes。 でも何に対して難しいか、 UMLや従来の手法が易しいのか、私に言わせれば、従来 の手法に UMLでも、かなり大きなシステムを作っても難しい、しかも形式手法を使 うよりもさらに難しい。そもそも、ソフトウェアを作ることが易しいことではなく 難しいこと。高々数100行のプログラムであれば難しくはないが、やはり何万行以上 ともなると、ちょっとやそっとのことではできない。 形式手法は誰でも使えるのかと言うと、No。 やはりソフトウェア科学や工学の知識が必要である。ただし、形式手法が誰でもで きないからと言って、従来の手法で誰でも開発ができているかと言うと、開発現場 ではできていない。 形式手法を使うと楽になるとは言わないが、人が亡くなるというような悲劇だとか、 プロジェクトで過労で倒れるようなことが、かなりの率で減らすことができる。 それなりに難しいが、やっただけの見返りがある。 質疑: Q.業務をほとんど知らない人でも作れたのなぜか? (藤倉) A. 1つは事務処理自体は、例えば、証券業務でも、普通にお金や証券の動きは多少 　説明を受ければ理解できる。 Q. VDMによる仕様作成で、曖昧なところがあぶり出されたわけだが、それは、やは 　り数式で書いたためか? (藤倉) A.数式というか仕様記述言語として、形式を組立てるという理由もあるが、仕様記 　述言語において、言葉すべてに対し、これは何であるかと正確に定義しなければ 　ならないため、類似する言葉の違いなどを正確に理解する必要があり、結果曖昧 　な部分が分かってくる。 Q.組込みの分野でもドメイン知識が必要であるが、それは、日本語で書いてあると 　曖昧さが生じるので、形式的に記述しておくべきなのか? (藤倉) A.まず、ドメイン知識の問題は何かと言えば、専門家の頭の中にあり、日本語にさ 　えにもなっていないことにある。実際書けないのかと言うと、これまでの例のよ 　うに書けるのに、今まではその専門家に聞かなければ分からなかった。 　しかし、例のように書けば、新人でもちょっと教えれば、何をしているのか分か 　る。形式的に記述すれば、業務知識、専門知識が伝えられるようになる。そもそ 　もドメイン知識が専門家の頭の中に隠れていることが問題なのである。 Q. VDMの場合、それを記述して、その後どうするか? (藤倉) A.実際、仕様を証明することができるし、テストデータを与えて、仕様をインター 　プリタで実行してチェックできる。またモデルチェック機能はないが、デッドロ 　ックくらいなら検出できる。 ＝＝＝ 関本:(SDLツールベンダー) SDLという言語はあまり聞いたことのない言語ではないだろうか。まずは、この言 語と自体の紹介を含めてお話ししたい。 、私自身は元々、半導体の制御系・通信系のソフト開発をしていた。そこでは、リ アルタイム系をオブジェクト指向で開発していたのだが、あまり良い C++のコンパ イラがなく Cで開発を行っていた。 その後、 SDLというツールに出会い、状態遷移モデルをシミュレーションし、コー ド生成して動いてしまうところに凄みを感じた。 もちろん、リアルタイム系の状態遷移系で書いていたので、 SDLを使えば上手く行 くと感じた。 SDLという言語は、SがSpecification、DがDescription、LがLanguage のことで、 一見、仕様を書くためだけの言語と見られるが、実際、 SDLは特にプロトコル系で は、プログラミング言語に入ってしまう。SDLはITU-Tというところで決まっている 言語である。 国際的に通信というものはネットでやるものなので、プロトコルの仕様を書かなけ ればならない。その時に、仕様を自然言語で書いてしまうと、やはり解釈が異なっ てくる。形式的な言語で書かなければならいない。そこで生まれたのが、SDLである。 特徴は、 UMLから詳細設計ができ、オブジェクト指向に対応する。また実装環境に 依存しない。ソフトとハードの関係する部分を記述できる。例えば、プロトコルで はレイヤ1 という物理層を取り扱うことができる。第3世代の携帯電話やBluetooth、 IEEEの無線LANなどの開発で実際に使われいる。 具体的にどんな言語かと言うと、ブロック分け、モジュール分けをして記述する。 システム全体を大きな四角で書き表し、その中にモジュールを階層的に書いていく。 そのモジュール同士の間でどんなイベントがやり取りされるか記述する。こうした 場合、(階層構造の)末端の部分が状態遷移系となる。この状態遷移系をフローチャ ートの形でプログラミングする。細かい動作までフローチャートの中に書く。これ でプロトコルの動作をすべて書くことができる。これを基にコード生成し、実際の 商品を開発する。 SDLツールの特徴として、テストとしてシミュレーションができる。また状態とイ ベントからツリー状の状態空間を考えることができる。これを自動的に網羅的にテ ストできる。人間がテストしたのでは分からないようなデッドロックとか、あるい は、ユーザ定義の変数とかのチェックができる。実際、かなり自動的なテストをや っている。 形式言語として、SDLを紹介してきたが、実際、通信系ではMSC(要求仕様を記述)や、 TTCN(テスト仕様を記述)という言語も一緒によく使われている。これも、形式的な 言語である。 開発事例を示す。 SDLを使ったら一体どうなるか。実際、 SDLを使った開発経験者 0人で行ったところ、エラーの数が半分以下に減った。シミュレーションと自動テ ストでほとんどのバグを潰す。生産性については、初回ということもあって、 10% しか上がらなかった。開発規模が小さかったことも原因。 SDLやTTCNは、実は通信系だけでしか使われていない。しかも通信系でも、一部で しか使われていない。でも、UML2.0 の中にSDLやMSCが取り込まれている。TTCNは、 UMLの中でのテスト用の拡張仕様として取り込まれていく。 弊社では、これらを踏まえた次世代ツールをすでに発売している。 弊社としては、形式的手法というよりは、まずは形式言語の使用を勧める。 ^^^^ ^^^^ 質疑: Q.デッドロックなどは、フローチャートを記述すれば検出できるのか? (藤倉) A.フローチャートを書いてあげれば、自動テストができる。 Q.具体的な効果はあるのか? (藤倉) A.弊社はツールベンダーで特に何か開発しているわけではないので、詳細なデータ 　はないが、シミュレーションや自動テストなどで、早期のうちにエラーを検出で 　きる。 Q.フローチャートが実際に動くのか? (藤倉) A.自動でCのコード生成して、実際に動かす。 Q.フローチャートを書くだけだと、なんだか簡単過ぎて、詳細な記述できないので 　は? (藤倉) A.NECでSDL上でのコーディングルールを作っていて、例えば、こういう書き方をす 　れば、パフォーマンスが遅くなるとか、あるいはメモリ効率が良くなるとか詳し 　く書ける。 Q.SDLから変換したCは、私達が読んで理解できるようなものなのか? (会場) A.正直言うと、最初は辛いと思う。しかし、トレーニングコースで解説を受けたり、 　ツールを連携することで、読めるようになる。 Q.デッドロックを検出できるとのことだが、時相論理式のようなものを書くのか? (藤倉) A.式の表記方法は違うが、ほぼ同じようなことはできる。 Q.では形式的手法との違いは? (藤倉) A.形式的手法に関してはあまり詳しくないので。。。 　・SDLという言語がまず先に作られたのか? (水口) 　・SDLをサポートする機能として、検証機能などがある。 (関本) 　・モデルチェッカーの場合、わりと理論的な上手いアルゴリズムが、まず先にあ 　って、そのツールを実装したというくらいの違いではないだろうか。 (水口) 　・実際、モデル検査ツールはたくさんあるが、能力などを評価する手段とかはあ 　るのか? (藤倉) 　・異なるモデルチェッカーの間で、共通な評価ができるモデルがない。 (水口) 　・モデル検査ツールで扱うモデルには違いがある。 　　例えば、SPINだと並行記述、SDLだとフローチャートなどとモデルが違う。 　　逆に言うと、どういうモデルを書くかという違いが、ツールの違いになる。 (青木) Q.メモリが足りないことはないのか? (高橋) A.確かにモデルが大きくなればなるほど問題である。 　例えば、通信器のシステムでは、いきなり全体を全探索するのではなく、各モジ 　ュールごとに全探索を行う。それから、それら持ち寄って全探索はしないで、ラ 　ンダムウォークで、何百万何千万と探索する。システム全部を全探索することは 　無理だと思う。また、予め探索する部分を指定できる。こうした工夫をいろいろ 　とする。 ＝＝＝ 倉岡: (動的テストツールベンダー) 弊社では、15年程前からステートチャートからコード生成をやっている。特に弊社 のツールは、動的なテストをサポートする機能を充実させている。ツールの適用範 囲としては、上流工程の設計からテストをサポートしている。モデルの方からコー ド生成して、テストを行う。UML2.0には、13の図があるが、そのほとんどに対応し ている。比較的以前の形式記述の言語に比べ、表現能力を高めようとする傾向があ る。 例えば、組込み系でよく使われる状態遷移図に関しては、状態遷移図の継承ができ るようになっている。例えば、ある状態があったときに、それのサブパッケージと いうか、その性質を受け継ぎながら、もっと特化したモデルを簡単に作れるように なっている。ある状態をさらにもっと外部的に状態を加えることができる。 実装レベルまで、こういったモデルを使っていこうとすると、より高い表現能力を 求めていくのではないかと思う。たぶん、その結果、解析等が難しくなるので、こ のあたりは、バランスをとっていく必要がある。 ここで、UML2.0で新たに加えられたコンポジット図について。 まずソフトウェアをブロック化して、そのブロックをさらにある程度詳しく分解す ることで構造化していく。また組込み系にとって、 UMLの便利な点は、シーケンス 図の一部を抜き出して、別のシーケンスとして書くことができる。いわゆるシーケ ンス図の構造化ができるようになったので、抜き出したシーケンス図は何度も使い まわすことができる。 また、シーケンス図の縦の線がオブジェクトを表現するが、そのような複数のオブ ジェクトを1つの線にパックすることができる。1本にパックしたオブジェクトは別 のところでも使うことができる。このように様々な構造化を使うことで、ソフトウ ェアを簡単に書くことができる。 弊社のツールでは、まず状態遷移図、クラス図、オブジェクト図のようなソフトウ ェアの静的な構造を表現する図、または、動的な状態遷移図、フローチャートのよ うなアクティビティ図などからソースコードを生成する。 OSに非依存となっているが、どうやって非依存にするかは様々な方式があるが、弊 社のツールのやり方は、モデル化で生成するコードとOSの間に中間層を用意する。 実際、このようなツールを組込みの分野で使用する段階で、 1つ気になるのが、ツ ールを導入することで、リスクを持ってしまうことである。例えば、クローズなラ イブラリをリンクしたりする。弊社の場合、一部のソースコードを公開したりして、 なるべく導入し易くしている。 また実際のところ新規にすべてを作ることは少ないのではないかということで、リ バースエンジニアリングのエンジンもある。今回、試しに TOPPERSプロジェクトの JSPカーネルに対して、リバースエンジニアリングをかけた。C言語からもリバース エンジニアリングできる。 C言語というと、オブジェクト指向から離れた感じには なるが、実際には弊社のツールを使うと、変数や関数という概念もモデル化するよ うになっている。そのため、 Cのプログラマが形式的な状態遷移図によるモデルを 移行し易くなっている。ソースコードからリバースエンジニアリングしてモデルに 反映するようになっている。 状態遷移図(形式的なモデル)から、コード生成するツールなわけだが、では、ソー スコードは生成物であるため重要ではないのかと言うと、弊社は重要だと思ってい る。そのため、モデルからソースコードを生成するが、その生成したソースコード の変更をモデルに反映することができる。 この状態遷移図によるプログラミングというか、実装実現をなるべく従来の技術や 経験を生かせるような仕組みになっている。生成したソースコードはそのままPCの 上で動かすことできるし、もちろん、ターゲットの上でも動かすことができる。 動く様子をアニメーションを使って見ることができる。現在あるソフトウェアパー ツであるオブジェクトがどのような状態で待っているのか、どのイベントを待って て、そのイベントが来るとどういう動きになるのかを状態遷移図によって捉えるこ とができる。またオブジェクト間でどのような通信があったのかはシーケンスで捉 える。 実際にテストをしようとする時、簡単にテストできるように、操作パネルが容易に 作れるようになっている。手続きを指定すると、ブラウザの方に自動的に操作パネ ルが出て、確かめたいイベントを手で入力することができる。また実際、その動い ているプログラムはPC上でもターゲット上でも動かすことができる。JavaScriptな どで操作パネルを拡張することもできる。 このようにテストの環境をかなり整えている。 もう 1つのテストの環境としては、先程の手動によるテストも必要なことだが、予 めシナリオ(正常パスや異常パス)を書いておき、それを実行して間違いがないか検 証したいときに、そのようなテストの自動実行をサポートしている。 テストのシナリオとしては、シーケンス図を使い、そのシーケンス図を解析して、 誰がどのようなイベントを入れて、どのような結果が得られれば正しいのかを調べ る。先程の手作業で操作するためのテスト用のコンソールを使うと、結果はシーケ ンス図で出るので、それをテストケースとしてそのまま使うこともできる。実際に 実行して、最終的に何%のミスがあったのか、ユーザが作ったシナリオが何%の合っ ていたのかを調べることができる。 もっと網羅的な試験をやりたい場合、人間が考えつくテストケースは、やはり限ら れているので、いわゆるモデルから推測できるテストケースをすべて知りたい。そ れを、例えば、回帰テストで使いたい。これに対応するコンポーネントがあり、状 態、状態遷移、関数の呼び出し、イベントの生成、すべてをカバーするようなテス トケースを生成する。こういったカバレッジ用のツールは多くある。 従来のツールはソースコードをベースにやるわけだが、こちらの方はモデルベース で行う。また、どうしてもテストケースの数が爆発するので、最適なテストケース を絞り込むようになっている。 #ここでテストのデモンストレーション 形式的な手法は昔からあるわけだが、それが開発者の間でなかなか浸透していかな い。 1つは、例えば、ステートチャートで仕様書を書いても、それがすぐさまコー ドに反映できるわけではない。そのため、どうしても後回しにされ勝ちになる。 最後の最後に、お客様に提出するためだけに書いている。本来であれば、開発の途 中で、今自分たちがどんな状態にあるかを把握するために便利なものである。しか し、なかなかそのような使われ方がされていないのではないだろうか。こういった CASEツールを使うと、状態遷移図がそのままコード化されるし、状態遷移図上での テストが行えるので、開発者の方が図を書くモチベーションになる。 #さらにテストのデモンストレーション #ならびに、ツールのスナップショットを交えた説明 今回、結果としてツールの説明のような内容になってしまったが、 1つは、こうい った技法をどうやって使ってくれるのかということに弊社では力を入れている。 ただモデルの表現能力を高めたい。これは、シンプルに作るのが、いい場合もある し、やはりある程度、例えば、状態遷移図だとネストした状態遷移図を書いた方が 全体としてはシステムのまとまりがいい場合もあり得ると思う。これに対応するモ デルの表現能力は実現している。また、モデル＝プログラムのようなものなってい るので、開発者の方もモデルを記述するモチベーションになるのではないだろうか。 さらに、書いたモデルがそのままテストに使える。テストケースもモデルで書いて いるので、やはり、全体として開発者がモデルを書こうするモチベーションを高め ると考えている。 質疑: Q.静的なチェックはやらないのか? (佐原) A.静的なチャックにはあまり強くない。現状だと初期状態が何だとか、簡単なチェ 　ックしかできない。 Q.状態マシンを与えると、テストケースを生成することから、状態数が多いとテス 　トケースも膨大な数になると思うが? (藤倉) A.テストケースを生成する際に、タイムアウトを設定できるようになっていて、も 　し計算が終わらなかった時は、テスト条件を変えることになる。 Q.そのツール特有の手法と呼ばれるようなものは何かないのか? (佐原) A.単なるツールなので、どのような開発手法にでも対応できるが、やはり、通常、 　 UMLをスケッチとして書くような使い方と比べると、動かさないといけないため 　に、これでは動く動かないとかの目安のようなものはあるが、特に、〜法という 　名前はない。ツールを導入する際に用いる。 ＝＝＝ 向山:(ハードウェア設計者) ハードウェア設計に関する研究開発を行っている。特に形式検証の方をやっている。 ハードウェア設計で形式的検証をどうやって使っているかを紹介する。 ハードウェア設計の中のどこで形式的検証を使っているのか言うと、RTLとGate Levelの等価性を静的に検証することから始まった。これが非常に成功して、ツー ルの業界で形式検証のツールが確立した。次の胎動として RTLのプロパティ検証の 方に注目が集まる。研究レベルで行われていて、98年に最初の市販ツールが出たが、 まだそれほど普及しているわけではない。 これまでの技術的な流れをモデルチェッキングに絞って話すと、 ・1986年 CTL 検索可能な状態数 10の4乗 ・1990年 Symbolic Model Checking 検索可能な状態数 10の20乗 ・1999年 Bounded Model Checking 検索可能な状態数 10の300乗 になる。 個人的には、Bounded Model Checking(BMC)が実用化のためには有効であると考える。 最近の検証ツールの多くはBMCである。今日本で手に入る検証ツールリストを見ると、 ここ4,5年のものばかりで、要するに、非常に若い分野である。 使う側の状況に関して、実際の設計でどれだけ使われているかと言うと、いろんな 事例はあるが、主なところでは、 IBMは非常に積極的に行っていて、彼ら自身が発 表したものによると、実際の製品の設計にツールを使って検証したら、全部のバグ のうち、形式的検証で 24%のバグを見つけた。 Intelでは、設計検証にツールを用 いて、 100以上のバグを検出した。これは、他のどの方法でも見つけられなかった ハイクオリティなバグである。 NECでも、プロパティ検証ツールを作っていて、特徴としては、BMCを採用してエン ジンだけに注力していて、扱える状態規模的には、かなり頑張っていて市販ツール を上回っている。 実際の設計にも使っていて、机上チェックしていたところが、これで自動化されて、 開発がだいぶ高速化された。これの拡張として、C言語のソフトウェアのプロパティ 検証ツールを作成している。コアのエンジンは全く一緒だが、モデル化するところ で、プログラムスライシングやレンジ解析といったアブストラクションを実装した。 試してみたところ、フロッピーディスクのドライバで、デバイス部の誤りを発見し た。 いろんな事例があって結構使えているイメージはあるが、実は誰にでも使えるツー ルにはなっていない。それはなぜかというと、大きく分けて2つの問題がある。 一番大きな問題は検証可能な規模が小さいことである。回路を例に見ると、 1,0を 記録している素子があるのだが、例えば2個になると、1,0の組み合わせで 4状態に なる。普通は、これは数千とか何万とかあるので、ものすごい数の状態遷移グラフ になる。ソースコードに適用する場合を考えると、例えば、Integerの変数は2の32 乗の状態数が必要で何も考えずにモデル化すると、とても使い物にならない。 では、現状でどうやって使っているかと言うと、いろいろ苦労はしているが、 1つ はアブストラクションで、プロパティによって真偽に影響を与えない範囲で設計を 書き換えて、規模を縮小する。いろんな障害はあるが、ばっさりいらいない部分を 切り落として、何とか小さくする。それは非常に難しい。 検証エンジニアと呼ばれる専門のエンジニアが IBMとかにはいる。その人はどんな 人かと言うと、検証ツールの原理を良く知っていて、かつ、その設計の仕様も熟知 している。どんな風にすると、検証ツールがダメになるかというノウハウを持って たりして、専門的に手作業で対処する。 もう 1つは、ツールに合わせて検証可能な規模まで、ブロックを小分割する。その ブロック単位で検証する。ただ問題なのは、あんまり小さく分割してしまうと、そ の分割したブロックに対して、プロパティが分からなくなり、何を検証していいの か分からなくなる。 本当に興味のある検証したいことは、ブロックを跨るような大きなものである。さ らにもう 1つは、制約条件を付ける。そうすると、状態遷移グラフの枝をばさっと 切るようなイメージで規模が小さくなる。実際に社内の設計者の人に見せてもらっ たところ、制約条件が数十行あって、その下に検証したいプロパティがある。検証 してバグが出たときに何が悪いのか分からないので大変である。 規模的な問題を解決するには、どうしたら良いのか。 あまり良いアイディアはないのだが、 ・計算機が飛躍的に性能向上すること ・モデルチェックのアルゴリズムがすごい画期的なものが提案されること ・状態遷移グラフをモデル化するときに、なるべく小さく、 プロパティの真偽に影響を与えないで小さくする、これを自動化すること などが考えられるが、すぐにはできそうもないと感じられる。 もう 1個の課題としては、検証するときのプロパティの明確化である。実際に、設 計プロジェクトでプロパティ検証をやろうとした時に、何が話の出るかというと、 1つは何を検証してよいのか分からないとよく言われる。規模的な対策で、ブロッ クを小さく分割すると、どんな制約条件を与えてよいのか分からない。 もう 1つは、どうやってプロパティを書いたら、自分が書いた設計が大丈夫だと安 心できるか分からない。これに対する解は、 ・プロパティのライブラリ化 ・設計非依存の普遍的プロパティ ・設計方法論の変革 ・プロパティ検証はデバッグツールと割り切る ・プロパティ検証言語の標準化 などがある。 形式的検証を使って楽をするにはという、そもそものテーマに立ち戻って考えると、 プロパティ検証はまだ成熟はしていない。ただし、網羅的なチェックによるメリッ トは大きい。ツールが未熟だからといって使わないのは、もったいないのではと思 う。現状で何とか使うには、どうすればよいかと言うと、 ・然るべき準備を行い、然るべき用途に使う。 ・他のツールに組み込んで使う。 ・仕様レベルの検証に使う。 ・心構え ・従来の検証のプラスアルファとして使う。 ・バグ検出率を高めるツールとして割り切る。 ・100%の正しさを証明するものではない。 質疑: Q.NECの社内で自社用の検証ノウハウはあるのか? (会場) A. C言語ベースの設計を独自に行っている。 RTLよりも抽象度の高いレベルで行っ 　ている。 Cでプロパティを書き、そのレベルで検証して、その結果、凡例を Cで 　書く。このような市販ツールはないので、 要するに Cベース設計の統合環境を 　作るという位置付けで研究開発している。 =========================================================================== 感想: まずは、時間切れで3人のパネラが話せなかったことは非常に残念だった。多少工 夫の余地はあったかと思う。 本題の形式的手法に関しては、佐原氏の開発事例で述べられた通り、実にメリット は大きい。しかし、実際のところ、まだまだ開発現場で浸透していない印象を受け るので、今後も、このような開発事例を広める機会が増えることを期待する。 ツールベンダーの関本氏と倉岡氏は、開発現場で形式的手法を定着させるべく、環 境の充実を図っていたと思う。開発方法論はツールあってこそ成り立つ面があるの で、両氏の働きかけは重要である。しかし、具体的な形式的手法と各々のツールと の関連が明確でない部分があり、形式的手法を用いる利点を十分に伝えきれなかっ た感がある。また昨今、形式的手法の代名詞的な存在となったモデル検査ツールに ついては、その先駆者であるハードウェア設計での経験に興味が深まるところであ る。 向山氏は、モデル検査ツールの技術的背景や使う上での本質的な問題となる状態数 の肥大化について明確に説き、その対策を示した。これは、ソフトウェア開発にお いても非常に有益な内容だったと思う。