Distributed software has played a major role in recent decades. Its spread comes with the increased complexity in the development of such software. Concurrent execution and inter-process communication are common in distributed applications. Such programming elements are prone to errors hard to detect. This leads to difficulties in maintaining software quality. Model checking is a powerful technique to find faults in concurrent applications. However, most model checkers concentrate on stand-alone applications and lack the capability to handle distributed applications. This thesis introduces the concepts of I/O cache and process checkpointing. A series of approaches, based on these concepts, are implemented to support a model checker in dealing with distributed applications. All of these approaches concentrate on verifying a single process called system under test (SUT), treating other processes as peers. Verifying a single process has an advantage of scalability. The state space that must be explored is much more smaller than the composite state space of all processes in an application. As a result, the model checker can completely explore the single state space in reasonable time. The I/O cache provides an emulated I/O interface for the SUT. It allows communication between a SUT and peer since the computation results on the peer are stored in the cache, ready to be replayed. However, the I/O cache cannot perfectly imitate peers' non-deterministic behaviors, which render the cache contents imprecise. Accordingly, we apply the idea of process checkpointing and trade verification time for precision. Checkpointing tools allow multiple peer processes to be backtracked in sync with a SUT. They can also be used to suppress non-deterministic behaviors of peers. An implementation of each approach has also been done as an extension for Java PathFinder, a Java model checker. We succeed in verifying an extensive class of distributed applications, e.g. a multi-process HTTP/SSH server, client and a download manager program. The proposed approaches are also compared to one another in term of important properties in software verification, e.g. soundness and completeness. The classes of SUT/peer applications supported by each approach are discussed as well.

ローカルエリアネットワークやインターネットの成熟により、クライアント・サーバモデルに基づくアプリケーションなど複数のプロセスがプロセス間通信しながら協調する分散ソフトウェアが普及している。これら分散ソフトウェアにおいて、それぞれのプロセス実行に非決定性が存在する場合、従来の検査手法を用いて分散ソフトウェア全体の瑕疵(バグ)を発見するのが難しくなっている。一つの独立したプロセスのバグを発見する手法としてモデル検査がある。モデル検査器が扱う検証対象(System Under Test: SUT)は一つのプロセスのみであり、そのプロセスが他のプロセスと通信して処理されることを想定していない。

本論文ではモデル検査器の対象を分散ソフトウェアに拡大するためにブランチングI/O(入出力)キャッシュとチェックポインティング機構の概念を提案し、これらの概念に基づいた一連の解決手法を提案実装し、評価している。本研究では一つのプロセスの検証に焦点を当て、通信している他のプロセス群の検証は行なわない。一つのプロセスにおける状態空間のみを扱っているために、分散システム全体の状態空間に比べてはるかに小さくなるために検証が一つのプロセスにおける状態空間に収まる。これにより、状態空間を爆発させずに網羅的に探索することが可能となった。入出力キャッシュはSUTの入出力インターフェイスとして働き、通信相手への送信とそれに対応する受信を保存する。SUTがバックトラックして通信相手に以前送信したデータと同じデータを送信した場合、その時に受信したデータを使うことにより、SUTは通信相手にデータを送ることなく同じ動作を繰り返すことが可能となる。しかし、SUTがバックトラックして通信相手に送った送信データと異なるデータを送る場合には、入出力キャッシュを利用することが出来ず、通信相手プロセスもバックトラックして処理を行う必要が生じる。このために、チェックポインティング機構を用いて通信相手のプロセスをバックトラックさせる手法を提案している。これにより、複数の通信相手を、SUTに合わせてバックトラックさせることが可能になる。

本論文は9章から構成される。第1章では、分散ソフトウェアにおける検証の難しさ、本論文の基礎となっているモデル検査、本研究以前に研究されていた研究の紹介がされ、本研究の貢献の概要が述べられている。提案されているモデル検査手法はモデル検査器であるJava PathFinder(JPF)を拡張し、かつ、既存チェックポインティング機構を基に実現されている。第2章は本論文の背景としてJPFの概要およびチェックポインティング機構で使用したツールの概略を説明している。また、既存研究でおこなれていた入出力キャッシュ機構を解説し、その限界について言及している。第3章は分散ソフトウェアのモデル検査を存入出力キャッシュ機構を基にどのように拡張していくかについて論じている。第4章では提案手法であるブランチング入出力キャッシュ機構を提案している。ブランチング入出力キャッシュ機構により非決定性を有するSUTのモデル検査が可能となった。しかし、この機構だけではバックトラックするときに通信相手のプロセスを最初から立ち上げなおす必要が生じ効率が悪くなる。そこで、第5章では通信相手のプロセスをチェックポインティングすることにより再実行するときのコストを軽減する手法を提案している。第6章では提案した手法の実装について述べている。第7章では開発した検証システムの評価として、非決定性を持つサーバ・クライアント、HTTPサーバ・クライアント、SSHサーバ・クライアントといった分散ソフトウェアの検証を確認した。また、チェックポインティング機構として、Virtual Machine、ユーザプロセスレベルで実装されているMTCPおよびDMTCPを用いた時の性能とそのトレードオフについて論じている。第8章では関連研究として、モデル検査器、ソフトウェアテスティング、仮想化技術、プログラム再実行手法についての既存研究を紹介している。第9章では本論文をまとめるとともに将来研究について述べられている。また、第4章および第5章において提案したモデル検査手法の完全性や健全性について、対応可能なSUT、通信相手の種類についても論じている。

従来手法で分散ソフトウェアを検証しようとすると分散ソフトウェア全体を検証するしかなく検証自体が非現実的だった。本論文で提案されたブランチングI/O(入出力)キャッシュとチェックポインティング機構により、他のプロセスと通信しているプロセスに対するモデル検査が限定的であるが可能とした。このことは、分散ソフトウェアの検証に対して多大な貢献をしているといえる。

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