SPIN モデル検査
検証モデリング技法
著：中島震
内容紹介
SPINの基礎から実際の利用方法までを具体的に解説する日本で初めての書籍 ◆SPINとは？ 社会の様々なところにソフトウェアが組み込まれ、その規模が飛躍的に大きくなってきている中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況が出てきている。 そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。限られたテストケースでの誤りの無さを保障する従来のテスト手法に対して、数学的・論理的基盤に基づいて正しさを証明するモデル検査法は、無限に近い組合せに対しても正しさを保障できる手法であり、その中でもSPINは実際に産業界での適用事例も豊富で、その技術習得がソフトウェア技術者の必須要素として注目されてきている。
目次
第1章 モデル検査とは―自動検証とモデル検査法 第2章 SPINを使ってみよう―Promelaの書き方とコマンドの使い方 第3章 性質を表現する―正しさの基準 第4章 対象を広げる―Promelaの実行規則 第5章 仕組みを理解する―SPINの検証法 第6章 ケーススタディ(1) ソフトウェアデザインを検証する―状態遷移ダイアグラムの解析 第7章 ケーススタディ(2) モデル検査を使い分ける―Java並行プログラムの解析 第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う―システムソフトウェアへの適用 第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ―抽象化の方法 第10章 ケーススタディ(5) デザイン検証の実際を知る―分散コンポーネントの振舞い検証
JP-eコード：76490353110000000004
。出版社：近代科学社
。コンテンツ公開日：2008年04月01日。