impress Direct SPIN モデル検査

ようこそゲストさん

｜

　はじめての方へ｜

　ご利用案内｜

　FAQトップ｜

　買い物カゴ｜

ご利用案内

配送状況確認はこちらから

【ご注意】
掲載商品の商品名、発売日、価格、内容などは変更になる場合がありますので、あらかじめご了承ください。

近代科学社ブックストアトップ　>　情報工学　>　ソフトウェア工学

検証モデリング
SPIN モデル検査

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

◆SPINとは？
社会の様々なところにソフトウェアが組み込まれ、その規模が飛躍的に大きくなってきている中、従来その信頼性を確保するための手法であったテスト手法は、時間やコストなどの面で開発の現状に追いつけない状況が出てきている。
そのテスト手法に代わるものとして注目されてきているのが形式的手法による検証（モデル検査法）であり、その中の一つがSPINである。限られたテストケースでの誤りの無さを保障する従来のテスト手法に対して、数学的・論理的基盤に基づいて正しさを証明するモデル検査法は、無限に近い組合せに対しても正しさを保障できる手法であり、その中でもSPINは実際に産業界での適用事例も豊富で、その技術習得がソフトウェア技術者の必須要素として注目されてきている。


著者：	中島震（国立情報学研究所教授）
品種：	書籍
ページ数：	256
サイズ：	B5変
発行：	近代科学社
商品ＩＤ：	KD0353
ISBN：	978-4-7649-0353-1

発売日：	2008.04.16発売
販売価格：	3,990円 (税込)
	ポイント10％還元
	(399ポイント)
在庫状況：

第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クイック・レファレンス
コラム　モデルのいろいろ／デッドロックの発生／LTLとCTL／無限長の受理列／SPINの工夫／NextオペレータとSPIN／MealyマシンとMooreマシン／UMLステートダイアグラム／スケジューリング・ポリシー／DbCとPDA／時間について

本サイトのご利用について｜お問合せ｜プライバシーについて｜特定商取引に基づく表示｜個人情報保護方針｜会社概要｜インプレスグループTop｜