ネットワークのインフラストラクチャを含むセイフティ・クリティカルなシステムが増えるに従って,ソフトウェア検証の重要性は今後ますます大きくなって行くと考えられる.状態の自動的な探索を基礎とするモデル検査法は,検証技術の一つとして,ハードウェア検証の分野で広く利用されており,ソフトウェアの検証に対してもその利用が期待されている.しかし,ソフトウェアはハードウェアに比べて状態空間が巨大であり,ソフトウェア検証に対してモデル検査法を直接には適用できない場合が多い.従って,ソフトウェアのモデル検査を成功させるためには,状態空間を小さくする技術が不可欠である.状態空間を小さくする最も重要な方法の一つとして抽象化があり,ハードウェアのモデル検査に対しては成功している.本論文は,ソフトウェア検証を行うために,抽象化の技術を付加したモデル検査法,すなわち,抽象モデル検査法について探求することを目標としている.

　本論文の第3章では,モデル検査法における抽象化の有効性を調べるために,一つのケーススタディとして,並行ごみ集めのアルゴリズムの検証を行う.並行ごみ集めアルゴリズムの正しさは簡単に証明できるものではなく,抽象モデル検査のような自動検証が有効な手段となる.このケーススタディを通じて,抽象モデル検査における二つの重要な課題が明らかになる.一つは,抽象化によって元のアルゴリズムの性質が失われないことを保証する理論的基礎が必要なことである.もう一つは,問題に応じて適切な抽象化をどのように構成するかという課題である.

　第4章では,抽象モデル検査の理論的基礎を与える.プログラム意味論の分野で研究されていた詳細化の理論を適用することによって,モデル検査と抽象化の関係を理論的に解明する。

　並行ごみ集めアルゴリズムを検証するケーススタディでは,ヒープの状態を抽象化する必要がある.ヒープは複雑なリンク構造を成し抽象化の可能性も無限にあるため,ヒープの抽象化をどのように定義すべきかは自明ではない.第5章では,リンク構造を抽象化するための一般的な技術を開発する.正則表現を用いることにより,並行ごみ集めアルゴリズムの抽象モデル検査に用いた抽象化を一般化する.この技術は,第3章で与えた二番目の課題の一つの答えになっている.

　モデル検査法は,与えられたソフトウェアが仕様を満たしているかどうかを自動検証するだけでなく,与えられた仕様を満たすソフトウェアを自動合成する問題にも適用可能なことが期待される。第6章では,アルゴリズムを自動合成することを目標に,モデル検査を用いてアルゴリズムの探索を行う方法を提案する.そのケーススタディとして,並行ごみ集めのアルゴリズムと排他制御のアルゴリズムの発見を試みる.第7章では,アルゴリズムの探索の効率を上げるために,シンボリックなモデル検査法をアルゴリズムの集合に適用する.この方法を用いることにより,モデル検査の一回の実行でアルゴリズムの集合を探索することが可能である.さらに探索空間を小さくするため,この方法に抽象化技術を適用する.すなわち,シンボリックな探索と抽象化を組み合わせる.この方法のケーススタディとして,相互排除のアルゴリズムの探索を行う.

　最後に、抽象モデル検査法の全プロセスの正しさを形式的に証明することを目指す研究について述べる.特に,抽象モデル検査で用いられる抽象化は,抽象モデル検査全体の正しさを保証するために,いくつかの条件を満たしていなければならない.理想的には,これらの条件は形式的に証明されるべきである.第8章では,並行ごみ集めの抽象モデル検査で用いられた抽象化の正しさの形式的証明を与える。形式的証明は,HOLと呼ばれる証明支援系の上で開発された.形式的証明と関連して,第9章では,証明支援系のための環境に関する研究についても述べる.まず,証明支援系のユーザ・インタフェースのためのガイドライトして,"proving as editing paradigm"と呼ぶ考えを提案する.このガイドラインは,第8章の形式的証明に際して実際に活用されたものである.また,プログラム意味論の分野で頻出する可換図をそのまま扱うことのできるグラフィカル・ユーザ・インタフェースについても述べる.

システム状態の自動的な探索を基礎とするモデル検査法は,システムが正しく動作することを検証する技術の一つとして,ハードウェア検証の分野で広く利用されている。一方、セイフティ・クリティカルなソフトウエアシステムが増えるに従って,ソフトウェア検証の重要性はますます大きくなり、モデル検査法をソフトシステムの検証法として用いることが期待されている。しかし,ソフトウェアはハードウェアに比べて状態空間が巨大であり,ソフトウェア検証に対してモデル検査法を直接には適用できない場合が多い。従って,ソフトウェアのモデル検査を成功させるためには,状態空間を小さくする技術が不可欠である。

本論文は、ソフトウェア検証を行うための抽象化の技術を付加したモデル検査法,すなわち,抽象モデル検査法についての新しい知見を報告したもので、全体は10章より構成さている。はじめの2章においてソフトウエア検証の重要性とモデル検査法の発展等を述べ,終章の第10章では、結語と将来の研究方向を述べている。

第3章では,モデル検査法における抽象化の有効性を調べるために,実用性においても重要であり、かつアルゴリズムの正しさがわかりにくい,並行ごみ集めのアルゴリズムをとりあげ、それにモデル検証法を適用し問題点を検討している。この結果、抽象モデル検査における二つの重要な課題を明らかにしている。一つは,抽象化によって元のアルゴリズムの性質が失われないこと保証するという課題であり、今ひとつは、問題に応じて適切な抽象化をどのように構成するかという課題である。

第4章では,上の第一の課題に答えるもので、抽象モデル検査の理論的基礎を与えている。ここでは、プログラム意味論の分野で研究されていた詳細化の理論を適用することによって,モデル検査と抽象化の関係を理論的に解明している。

第5章は、第3章で述べた二番目の課題の一つの答えを与えている。並行ごみ集めアルゴリズムを検証するケーススタディでは,ヒープの状態を抽象化する必要がある。ヒープは複雑なリンク構造をしており抽象化の可能性も無限にあるため,ヒープの抽象化をどのように定義すべきか自明ではない。本章では、リンク構造を抽象化するための一般的な技術を開発し、正則表現を用いることにより,並行ごみ集めアルゴリズムの抽象モデル検査に用いた抽象化を一般化している。

第6章では,アルゴリズムを自動合成することを目標に,モデル検査を用いてアルゴリズムの変種を探索する方法を提案している。

第7章では,アルゴリズムの探索の効率を上げるために,シンボリックなモデル検査法をアルゴリズムの集合に適用している。この方法を用いることにより,モデル検査の一回の実行でアルゴリズムの集合を探索することが可能となる。さらに探索空間を小さくするため,この方法に抽象化技術を適用している。

最後の2章においては、抽象モデル検査法の全プロセスの正しさを形式的に証明することを目指す研究について述べている。第8章では,並行ごみ集めに対する抽象モデル検査で用いられた抽象化の正しさを、形式的に証明している。形式的証明は,HOLと呼ばれる証明支援系の上で開発された。

第9章では,第8章でもちいたHOL証明支援系のための環境に関する研究について述べており、"proving as editing paradigm"と呼ぶ考えを提案している。この考えは,第8章での形式的証明に際して実際に活用されたものである。また,プログラム意味論の分野で多く使われる可換図をそのまま扱うことのできるグラフィカル・ユーザ・インタフェースについても述べている。

以上要するに、本論文は、ソフトウエアやアルゴリズムの正しさを検証する手段として、モデル検証法を用いる際に大きな問題となっていた状態数の爆発的増加を、抽象化の技法を援用することにより軽減する方法を提案し、それを発展させたもので、理学上の貢献が大と言える。なお、本論文の第3、5,6,7,9章は萩谷昌巳氏と、また第4、9章は木下佳樹氏との共同研究であるが、論文提出者が主体となった研究であり、本人の貢献は十分であると考えられる。よって、本論文は理学博士を与えるに十分な内容を有すると判定した。