並行システムの検証と実装を読んだ
序
CSP(Communication Sequential Process)というプロセス代数とそれに基づいた形式手法の本を読みました。頑張って読んだので紹介します。
CSPは並行計算をラベル付き遷移システムで表現した上で(これをプロセスという)、どのような遷移がありうるのか、プロセス間の遷移(の集合)にどのような関係(e.g. 詳細化関係)があるかを議論する枠組みです。
自動検証器の実装がいくつか知られていて、この本ではFDRを使ってモデリングと検証を行う方法が説明されています。
この本はCSPというプロセス代数の一種と、その理論に基づく検証手法と検査器について説明している教科書です。
トップエスイーで使っているようです。ほとんど前提知識は不要です。
読み切るとCSP(m)の簡単な構文と意味が頭に入り、実際に使える検証器であるFDR4も使えるようになります(文中で説明されるのはFDR2なので大分趣が変わりますが簡単に対応は付きます)。
書評
全体について
インクルーシブで前提知識がほとんど要らないのが良いです。Javaが読めることくらいでしょうか。
また同じ前提から導出されますが、本文中で説明する気のない無意味に高度なトピックや定理に触れたりしないのも良い点です。書いてあることは全部本の中で完結します。快適。
関連する話題として、練習問題がちゃんと練習になっており、ちゃんと解答があるのも良い点です(当たり前だとは思ってるけどこの手の教科書には期待出来ないので)。
各章について
まず5章と6章が読んでいて楽しいです。
形式的な遷移規則を使って遷移の導出をする説明がされ、詳細化関係についても定義が形式的に提示されるので分かり易いです。
またそれらを使ってどういう手順で証明をするのかについて繰り返し説明があるので、読んでちゃんと手順をなぞるだけで(大体)頭に入ります*1。
ただCSP規則(書き換え規則?)を用いた等価関係の証明については一部の規則が提示されるだけでさほど説明は無いのがやや残念でした。
(この本の主眼はFDRを用いた詳細化関係の検証なので構成上は妥当)
4, 8, 9, 10 章(全体で10章の構成)はJCSPというJavaライブラリを使ってCSPで記述したモデルをJavaで実装する方法を説明しています。
多分トップエスイーでは検証と実装が繋がっていることをちゃんと示さないといけないでしょうから仕方無いんですが、やや多いですね。
単にライブラリの使い方を説明しているわけではなく、実装するに際して発生しうる問題に対応するモデリングの方法論やテクニックが述べられてはいます。
また、タイムアウトや割り込み演算子など理論の章では扱っていないものについても適宜紹介されていて興味深いです。
が、JSCP というライブラリはメンテされているのかすらよく分からない様子で、公式サイトにもほとんどリポジトリへのリンクがあるだけです。
ライブラリという面から見ると本気で使わせるつもりがあるのか疑問という感じです。
こういう状態に加えて、理論には含まれていない実装における制約がいくつもあり(選択の可否とか送受信する値の型とか、ガードに使えるか否か、etc...) 少し読むのがツラかったです。
実装に直接対応取りたい人は興味のあるところだとは思います。
まとめ
全体として良い本です。
まず独学で読み通せるというのがポイント高いです。
また一貫して似たような例の変種を丁寧になぞって説明してくれるので、「先の例と同様なので自明。オワリ。」みたいな箇所も皆無で躓きづらいだろうと思います。
正誤表
読む過程で見つけたエラッタを書いておきます。私が読んだのは初版(2012/12/31)。
セクション | ページ | 誤 | 正(多分) |
5.3.1 | p.160 | 次のように定義されているする | 定義されているとする |
5.3.1 | p.163 | 視覚的に確認するツールPorBE | 視覚的に確認するツールProBE |
7.4.3 | p.248 | Counter(a, b) は | Counter(a, d) は |
7.4.3 | p.248 | 上司への支払い指示 tell.N と | 上司への支払い指示 bill.N と |
7.4.3 | p.253 | 1番目のコイン Crypt(1) を | 1番目のコイン Coin(1) を |
10.2.2 | p.324 | length(s^t) <= Size | length(s^t) <= size |
*1:ホントか?