本文へジャンプ

混沌から構造をつむぐ「モデル検査」

 萩谷先生も、ずいぶん広範囲な研究をしていらっしゃいます。いまはどんなことを?

いろいろ節操なくやっていますね、ふふ。形式手法(数理的技法)という分野があります。簡単にいえば、論理学を応用して、バグ(間違い)のないプログラムをつくったり、バグを見つけたりするための方法論のことです。それを研究しています。

形式手法で、プログラムの開発方法は変わるのですか?

正統的な形式手法では、形式的な仕様を書いて、それを満たすようなプログラムをつくりだす。で、そういう形式仕様がついたプログラムを組み合わせて、大きいプログラムをつくるというものです。ひとつの理想形。

その一方で、あるがままの既存のプログラムを頑張って検証するアプローチがあります。「モデル検査」というアプローチなのですが、私たちもモデル検査やそのための抽象化を研究しています。最近は、産業界からも関心が集まっているんですよ。いろんなツールが開発されてきています。新しくできた小林研究室も、モデル検査、特に高階モデル検査を本格的に研究していますよ。

モデル検査とはそもそも何なんですか?

プログラムがつくる状態空間を網羅することが基本です。というと、すごく難しく聞こえるかもしれませんが、要するに、プログラムのあらゆる可能な実行経路を、すべてしらみつぶしに調べるということです。そして、エラーの状態にたどりつかない、つまり、エラーは絶対に起きないということを保証するんです。

ずいぶん乱暴な方法ですね。これまでのプログラムのテストとどう違うのでしょうか?

プログラムのテストは、通常は代表的な入力に対してしか行われません。だから、テストを通っても、エラーが絶対に起こらないということは保証できません。これに対して、モデル検査はすべての可能な入力に対してプログラムを実行します。

そんなこと、可能なんですか? 入力の可能性は無限といってもよいですよね。

そうです。そのうえ、プログラムの状態の組み合わせは膨大だから、単純にやったのでは時間がかかりすぎて、絶対に検証は終わりません。力づくの計算をいかにやってのけるか、そこがポイントですね。短い検証時間、少ないメモリですませられるようにするには、プログラムやデータに潜んでいる規則性をうまくとらえられるかどうかが、カギになります。

つまり、モデル検査によって完璧な検証を行うためには、プログラムやデータに内在する規則性をとらえ、無限の可能性を有限、しかも、なるべく小さい有限に還元することが必要になります。たとえば、あんまりよい例ではないんですが、プログラムコードをカット&ペーストしていたら、そこは同じような構造になりますよね。それも、プログラムの規則性の一種です。

そういうプログラムやデータに内在する規則性を見つけて、規則性にしたがって、同じ構造、似たような構造を1つにまとめる。それが抽象化です。抽象化によってプログラムはすごく単純になり、モデル検査が現実的に可能になります。人間には、プログラムの本質的なところが見えてきます。

ですから、モデル検査の分野では、規則性を見つける、規則性を表現する方法を見つける、もしくはその「見つける」ということ自体をプログラムで自動化する方法を考える。そういうことを、みんなやっているんです。

なんだか、物理学みたいですね。森羅万象、じっと見つめるとマクスウェル。わけのわからないもののなかに真理―原理や通則を見つけて、その真理を説明したい、数学的に証明したい、というわけですね。

そうそう。わけのわからないプログラムでも、それなりの規則性が内在します。それをきちんと見いだして説明できれば、結果として自動的に検証ができるんです。その課程は、圏論の抽象的なものを積み上げていく楽しさに通じますね。

実は、抽象化の手法にはいろいろなところに適用できるという広がりがあって、そこも面白いんです。たとえば、生物のいろいろなシステムにも同じような手法が適用できそうだということになります。

抽象化は、特定の問題への個別の解ではなくて、普遍的な手法であると。そして、生物コンピュータへと続くのですね?

うんうん。だんだんチューリングの晩年に近くなってきましたね(笑)。

抽象化に関しては、ちょっと面白い話があります。私はこれまで、DNAコンピューティングといって、簡単にいえばDNAでコンピュータをつくる研究をやってきました。DNAコンピュータのメカニズムは、DNAという高分子の化学反応系なので、DNAがもつ組み合わせ的な複雑性を受け継いでいます。

その一方で、最近、RNAiといって、RNAによる遺伝子制御の仕組みをモデル化してシミュレーションする研究を、さきがけの研究者とやっています。RNAとDNAは兄弟の分子ですよね。DNAとRNAのもつ組み合わせ的な複雑性のために、DNAコンピュータやRNAiの動作をシミュレーションするためには、何らかの抽象化がどうしても必要になります。

そこである種の抽象化を定義したんですが、実はこの抽象化が、ずいぶん昔にLispやJavaなどのガーベージコレクション※4のアルゴリズムをモデル検査によって検証したとき用いたものと、非常に似ていたという話でした。

※4:ガーベージコレクションは、プログラムが実行中に獲得・使用したあとの空きメモリを、整理・解放して再利用できるようにする仕組み。

ページトップへ戻る