クリプキクローネ日記帳

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

スポンサーサイト

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

SPINモデル検査 検証モデリング技法 [中島震(著)] (近代科学者)

前回に続きSPINの本です。
というより、両方同時に読みました。
途中まで読んで「よく分からないな」と思ったらもう片方の本を読んで、
ふと元の本に戻ると分かるようになっている、ということが何回かありました。
1つの内容の本を2冊同時に読み進めるのは結構ありかもしれません。
片方の本だけに載っている話も多かったので両方読んで正解でした。


本書はまず1章でモデル検査全体の概要が説明されているので貴重です。
SPINの位置付けが少し分かります。

そして具体例とオートマトンの図が豊富なので、意図がスムーズに入ってきて読みやすいです。
が、前回紹介した本と比べるとPromelaの言語仕様の説明が少ないのでそこで若干つまづきます。

あと、LTLの論理式からBuchiオートマトンを生成して充足可能性を検査するタブロー法が
システマチックにきちんと説明されていて、とてもすっきりします。
時相オペレータの数とそれ以外の論理記号の数で二重帰納法を回したくなります。
変換だけ見ると時相オペレータの数が減っていないので一瞬あれ?と思いますが、
その部分は再帰的な定義になっているので新しいノードにならないのも気分がいいです。

そして本の後半はかなり多くのケーススタディがあります。
Javaのスレッド間同期の話や、組み込みのタスク優先度の話、特に火星探査機Mars PathFinderの話、
UMLとモデル検査の話など、どれも興味深いです。
前回紹介した本と同様、教科書と実用書の雰囲気を併せ持つ良書です。

ここからは本の話ではなく、SPINや一般のモデル検査についての感想ですが、
割と素朴なオートマトンや数理論理が実際のソフトウェア設計に役立つという嬉しい気持ちと、
そうは言ってもやっぱり状態爆発や表現力の限界が多くて費用対効果としてなかなか厳しそうだなという気持ちが
両方入り混じった気持ちで読みました。

あとはやっぱりPromelaがC言語に似てるから余計に感じてしまうのですが、
モデル検査のためだけにPromelaのコーディングをするのではなく、
実際の実装から検証できれば適用範囲が格段に広がるだろうなと思いました。
最もそんなことは誰でも考えているわけで、既にそういう試みもあるようです。
ですが、Promelaでゼロから極力シンプルに書いてもオートマトンはすごい規模になるので、
実装コードから変換したらしたでやはり大きな壁にぶつかりそうです。

なんだかネガティブなことばかり書いてしまいましたが、
ソフトウェアの実用の世界でこうやって論理ベースで議論できる分野は少ないので、
とても貴重な分野だしもっともっと盛り上がるといいなと思います。
ついでに時相論理だけではなくて他の様相論理や他の非古典論理も
ソフトウェアの設計にダイレクトに結び付くようになったら最高だなと思います。
二階命題論理とかも述語論理より状態が絞れるしおもしろいと思うんだけどな。


  1. 2017/02/01(水) 00:47:05|
  2. | トラックバック:0
  3. | コメント:0
<<実践テスト駆動開発 [Steve Freeman, Nat Pryce(著), 和智右桂, 高木正弘(訳)] (翔泳社) | ホーム | SPINモデル検査入門 [Mordechai Ben-Ari(著), 中島震(監訳), 谷津弘一, 野中哲, 足立太郎(共訳)] (オーム社)>>

コメント

コメントの投稿


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

トラックバック

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