SPINモデル検査―検証モデリング技法

著者 :
  • 近代科学社
4.25
  • (1)
  • (3)
  • (0)
  • (0)
  • (0)
本棚登録 : 22
レビュー : 2
  • Amazon.co.jp ・本 (238ページ)
  • / ISBN・EAN: 9784764903531

感想・レビュー・書評

並び替え
表示形式
表示件数
  • 近代科学社ウェブサイト
    http://www.kindaikagaku.co.jp/information/kd0353.htm

  • 初心者向けSPINの実用書です。

    SPINとは、"Simple Promela Interpreter"の略で、"Promela"は、Gerard J. Holzmannが作った並列処理を伴う状態遷移(オートマトン)を記述できる形式仕様記述言語のことです。
    この本は、実例(Promelaプログラムサンプル)を通してソフトウェアの振る舞いの形式記述法を学び、SPINでそれを動かしてデッドロックや、プロセスのプライオリティ逆転等々のモデルチェッキングの方法を学ぶことができます。

    SPIN自体は、プログラマが振る舞いの検証を行うために使うツールと思いますので、いわゆる第三者検証を実施しているテスト設計を行う人が使うことはないと思いますが、SPINでどんなことが検証できるのかを知っておくことは悪くないと思います。

    また、特に9章の「検査対象の大きさを適切に保つ……抽象化の方法」は普通のテスト設計にも非常に役に立つと思います。この章の始めに、抽象化が重要であることは容易にわかるが、抽象化によってシステムがもともと持っていた性質が消えてしまっては元も子もない。という文があるのですが、じゃあどういう観点で抽象化していくのと言う答えがこの章にあります。節名だけ書くと、
     9.2 データ値に着目した抽象化
     9.3 制御の流れに着目した抽象化
     9.4 連続時間の抽象化
    です。

    山本訓稔さんがリーディングされている「Model Checkingを適用した実践的非同期制御検証」は、要するにモデル設計フェーズで作成しているxUMLからPromelaを自動生成するツールを作ったってことです。
    こうすることで、xUMLからC++へ変換されるC++の3万行のコードに対して、300万もの状態を自動検証したことと同等の効果を得ることができ、きわどい欠陥を検出できています。

    つまり実用段階の技術となってきているのですね。

全2件中 1 - 2件を表示

著者プロフィール

中島 震 (国立情報学研究所教授)

「2015年 『Event-B』 で使われていた紹介文から引用しています。」

SPINモデル検査―検証モデリング技法のその他の作品

中島震の作品

ツイートする