内容説明
昨今、ソフトウェアの正しさを保証するソフトウェア検証の技術が重要視されているが、その中でも特にモデル検査が脚光を浴びている。それは数理論理学などに関する知識があまりない技術者にも、ソフトウェア開発の中で利用することが可能だからであろう。本書はSPINを中心にモデル検査をいかにしてソフトウェア開発のプロセスの中に位置づけるかについて実例を通して詳説している。
目次
第1章 設計モデル検証とモデル検査
第2章 モデル検査概論
第3章 モデル検査ツールSPIN概要
第4章 SPINによるモデル検査
第5章 SPINによる設計モデルの検証プロセス
第6章 設計モデルの検証の実際
第7章 検証の実践：抽象化・効率化・デバッグ
付録A PROMELA/SPINリファレンスマニュアル
付録B 設計モデルの検証プロセス
付録C 簡易ステートマシン図のシンタックスとセマンティクス
付録D 簡易ステートマシン図とPROMELAの対応
感想・レビュー
※以下の感想・レビューは、株式会社ブックウォーカーの提供する「読書メーター」によるものです。
明るいくよくよ人
0
ぱらぱらと斜め読み。上流工程にモデル検査をどのように取り入れていくかに関して、ネットワーク家電の例で記載。例が簡単なのか、筆者がモデル検査を上流工程に適用する際の課題が、例の中でどのように解決されていくのかが今ひとつつかめなかった。ただ、具体的に適用の仕方が示されているので、この部分は有用だった。SPINに関しては、あまり実用を示した本がない（と思うので）、全体的に脱稿が多い（特に、図版とかが抜けてる。TeXとかではないのかな）のが残念。2012/06/09
Q
0
モデル検査の解説書。SPINは古くからあるツールで、専用の仕様記述言語で振る舞いを記述し、C言語に変換した後、当該コードをコンパイルし実行することで、モデル検査を行なう。LTLも扱うことができ、本書ではLTLを一から説明してくれてわかり易かった。一方でUMLとオブジェクト指向言語とSPINを組み合わせた設計プロセスは運用するには重く、さらに既存実装に追加の機能要求があった場合にはちゃんとモデルから修正追従できるのかは疑問が残った。モデル検査は初期の基本設計の妥当性を担保するためにのみ有用なのではと感じた。2019/03/14
