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

関連サイト

本書の関連ページが用意されています。

• SPIN モデル検査（近代科学社ウェブサイト）

内容紹介

SPINの基礎から実際の利用方法までを具体的に解説する日本で初めての書籍

◆SPINとは？

社会の様々なところにソフトウェアが組み込まれ、その規模が飛躍的に大きくなってきている中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況が出てきている。

そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。限られたテストケースでの誤りの無さを保障する従来のテスト手法に対して、数学的・論理的基盤に基づいて正しさを証明するモデル検査法は、無限に近い組合せに対しても正しさを保障できる手法であり、その中でもSPINは実際に産業界での適用事例も豊富で、その技術習得がソフトウェア技術者の必須要素として注目されてきている。

書誌情報

• 著者: 中島 震
• 発行日: 2016-11-01 (紙書籍版発行日: 2008-04-16)
• 最終更新日: 2016-11-01
• バージョン: 1.0.0
• ページ数: 259ページ(PDF版換算)
• 対応フォーマット: PDF, EPUB
• 出版社: 近代科学社

対象読者

自動検証, モデル検査法, Promela, 拡張有限状態オートマトン, Promela言語に興味のある方

著者について

中島 震

1981年東京大学大学院理学系研究科修士課程修了。現在、国立情報学研究所教授・総合研究大学院大学教授　学術博士（東京大学）。
この間、科学技術振興機構さきがけ研究員（兼任）、北陸先端科学技術大学院大学客員教授を歴任。形式手法、自動検証、ソフトウェア・モデリングなどの研究に従事。

目次

第1章　モデル検査とは―自動検証とモデル検査法

• 1.1　振舞い仕様とモデル検査法
• 1.2　モデル検査法の発展

第2章　SPINを使ってみよう―Promelaの書き方とコマンドの使い方

• 2.1　簡単な並行実行プロセス
• 2.2　通信プロトコル

第3章　性質を表現する―正しさの基準

• 3.1　プリンタとスキャナ
• 3.2　時相論理を用いた性質表現
• 3.3　反駁のための記述

第4章　対象を広げる―Promelaの実行規則

• 4.1　拡張有限状態オートマトン
• 4.2　Promela言語の基本

第5章　仕組みを理解する―SPINの検証法

• 5.1　SPINのツール概要
• 5.2　オートマトンによる形式化
• 5.3　状態空間の探索法
• 5.4　時相論理との関係

第6章　ケーススタディ(1) ソフトウェアデザインを検証する―状態遷移ダイアグラムの解析

• 6.1　状態遷移システム
• 6.2　分散協調システム
• 6.3　バリエーション

第7章　ケーススタディ(2) モデル検査を使い分ける―Java並行プログラムの解析

• 7.1　デザイン検証とJavaプログラム
• 7.2　Javaの並行同期機構
• 7.3　入れ子モニターの不具合

第8章　ケーススタディ(3) 組込みソフトウェアの解析に使う―システムソフトウェアへの適用

• 8.1　割り込み処理と共有資源
• 8.2　リアルタイム・スケジューリング

第9章　ケーススタディ(4) 検査対象の大きさを適切に保つ―抽象化の方法

• 9.1　抽象化の重要性
• 9.2　データ値に着目した抽象化
• 9.3　制御の流れに着目した抽象化
• 9.4　連続時間の抽象化

第10章　ケーススタディ(5) デザイン検証の実際を知る―分散コンポーネントの振舞い検証

• 10.1　ドキュメントからのモデリング
• 10.2　システム記述と検査性質
• 10.3　まとめ

参考文献

Promelaクイック・レファレンス