4日で学ぶモデル検査 (初級編)

衝撃的なタイトル。モデル検査もこんな俗っぽいタイトルが付く程度に一般的なものになったのですね。科学の見事な勝利です。

本当に4日以下で読むことが出来ます。時相論理を扱っていますが、内容は非常に簡単でわかりやすい。初級編とありますが、本当に初級で、現実のシステムに応用できるまでには当然至ってませんし、本書を読んだ限りではどうやって応用するのか検討もつかないくらいです。

載っているPromelaやNuSMVのコードがあまりエレガントに感じられず、モデル検査とはこのような泥臭いものなのか、あんまりやりたいことではないなあと思ってしまいました。

中級編、上級編は果たして発売されるのでしょうか？