TOP > 情報工学
 □ ニュースリリース
コミュニケーション・
情報リテラシー
工学一般
情報工学
電子工学
数学
物理学
ビジネス・経済
建築・都市計画
科学一般
公立はこだて未来大学出版会
発行
ナノオプト発行
弊社の書籍はお近くの書店・大学生協でお求めいただけます。店頭にない場合はお店からお取り寄せもできます。また、インターネットでもご購入いただけますので各販売サイトをご覧ください。
  サポート
   正誤表、授業用の教材などが
   あります
  地図(インプレスグループ)
   Google Map


株式会社 近代科学社

〒162-0843
東京都新宿区市谷田町2-7-15
TEL : 03-3260-6161
FAX : 03-3260-6059

 
情報工学
 
検証モデリング
SPIN モデル検査

book

発売日:2008.04.16
定価:本体3,800円+税

アマゾンで注文

 

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

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

 
著者 中島 震(国立情報学研究所 教授)
ページ数 256
サイズ B5変型
ISBN 978-4-7649-0353-1
     
主要目次

第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 |
 Copyright © 2016 Kindai kagaku sha Co.,Ltd, an Impress Group company. All rights reserved.