クリプキクローネ日記帳

ある種の音楽と数学とランニングはミニマルなところが似ていると思う。

スポンサーサイト

上記の広告は１ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。
  1. --/--/--(--) --:--:--|
  2. スポンサー広告

SPINモデル検査入門 [Mordechai Ben-Ari(著), 中島震(監訳), 谷津弘一, 野中哲, 足立太郎(共訳)] (オーム社)

ソフトウェアのモデル検査ツールの１つであるSPINの本を読みました。
モデル検査というのは、ソフトウェアの仕様や設計をモデル化して、
そのモデルが所望の性質を満たすかどうかを検査しましょうという話題です。
たとえば２つのプロセスが並列に走るときにデッドロックにならないかどうか、とか、
クライアントがサーバーにAを送ったら必ずBが返ってくる仕様になっているはず、とか
そういうことを検査します。

そしてこういった条件は多くの場合、時相論理で記述します。
大学で数理論理学をやっていながらモデル検査はほぼノータッチでしたが、
実際に時相論理がどう使われているのか前から気になっていたので、今回本を読んでみました。
前置きが長い！

SPINでは、検査対象のモデルを専用言語Promelaで記述し、
検査したい条件を線形時相論理(LTL)で記述します。

このPromelaはとっつきやすいようにCっぽい言語になっていて、
さらにLTLの論理記号も&&, ||, ! のようなC言語の論理記号を用いるので、
ちょっと油断していると普通にCでコーディングしているように見えてきます。
仕様や設計のモデルを検査しようとしたらなぜかコーディングが始まってしまった、となりそうです。

ですが、実際に動いている仕組みはCとは完全に別世界です。
Promelaで記述したモデルは非決定性有限オートマトンに変換されて、
さらにLTLの論理式もオートマトンに変換されて、両方の充足可能性がガンガン探索されます。
力技です。

このオートマトンはすべての変数の値とすべてのプログラムカウンタが指す位置をセットにして１つのノードを作るので、
Promelaの記述を少しでも油断すると簡単に状態爆発します。
すごい世界です。

なので、検査したい性質に関係ない変数や要素は極力省いて、シンプルなモデルを心がける必要があります。
そうは言っても、世の中の特にリアルタイム系のシステムは大抵思わぬところが思わぬところに影響して不具合が出るので、
モデル化の際に何を盛り込んで何を盛り込まないかはすごく難しそうです。

さて、SPINの話ばかりで全く本の話をしていませんでした。
本書はこういったSPINの全体像の説明を基礎からしてくれるいい本です。
タイトルからはツールの使い方の本のような印象を受けますが、
時相論理、オートマトン、非決定性、果てはNP問題まで、
いろんな概念の説明を丁寧にしてくれるので、半分教科書のような雰囲気があります。
かと思えばハッシュテーブルの大きさの調整や半順序簡約などの最適化の話題もあって、実用書的な雰囲気もあります。
あとこの手の本にしては翻訳がすごく読みやすいので、著者が日本人でないことを忘れそうになります。

特に非決定性のところはPromelaとC言語の違いのキモなので、
繰り返ししつこく説明されていてとてもよかったです。
  1. 2017/02/01(水) 00:00:18|
  2. 本
  3. | トラックバック：0
  4. | コメント：0
<<SPINモデル検査 検証モデリング技法 [中島震(著)] (近代科学者) | ホーム | パーフェクトC# 改訂3版 [斎藤友雄, 醍醐竜一(著)] (技術評論社)>>

コメント

コメントの投稿


管理者にだけ表示を許可する

トラックバック

トラックバックURLはこちら
http://myumbrella.blog42.fc2.com/tb.php/346-2d93a9f7
この記事にトラックバックする(FC2ブログユーザー)
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。