並行システムの検証と実装(ヘイコウ システム ノ ケンショウ ト ジッソウ)

この一冊で、並行プログラミングの基礎理論、検証技術、実装手法が分かる。並行システムの CSP によるモデル化技術、モデル検証器 FDR による検証技術、 Java ライブラリ JCSP による実装手法を詳細に解説。

マルチスレッドや分散システムにおけるバグは、再現性が低く、テストだけでは見つけきれないことがあります。デッドロック、ライブロック、競合条件といった並行性の欠陥は、実行タイミングの組み合わせに依存するため、すべてのパスを手動で確認するのは事実上不可能です。本書はこの問題に対し、モデル検査という形式手法を用いて並行システムの正しさを機械的に検証する方法を体系的に解説します。

CSP (Communicating Sequential Processes) をベースにしたプロセス代数の理論を導入し、システムの振る舞いを形式的に記述したうえで、モデル検査器 (FDR や PAT) によって状態空間を網羅的に探索する手順を実例つきで示します。著者の磯部祥尚氏は産業技術総合研究所でソフトウェア検証の研究に携わっており、学術的な厳密さと実装寄りの視点が両立しています。

対象読者は、並行プログラミングの経験があり、テストだけでは検証しきれない不安を抱えているエンジニアや、形式手法に関心を持つ大学院生です。前提として離散数学や状態遷移の基礎知識が求められ、敷居は低くありません。しかし、「正しさを証明する」という発想を実務に持ち込みたい人にとって、他に代替が少ない貴重な日本語文献です。