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


株式会社 近代科学社

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

 
情報工学
 
トップエスイー実践講座3 モデル検査の実践ソフトウェア検証
SPINによる設計モデル検証

book

発売日:2008.09.26
定価:本体3,600円+税

アマゾンで注文

 

モデル検査の実践的活用!!ソフトウェアの欠陥発見、精度向上、効率化のノウハウを網羅!

「モデル検査と設計検証のノウハウを、SPINを使い、ネットワーク家電の開発を題材にして解説」「開発期間の短縮と高信頼性を実現するソフトウェア開発の指南!本書は単なるモデル検査の教科書ではなくSPINを実際にソフトウェア開発に利用するための解説書である。

 
著者 シリーズ監修:本位田 真一、監修:萩谷 昌己(東京大学大学院)
著者:吉岡 信和(国立情報学研究所)、青木 利晃(北陸先端科学技術大学院大学)、田原 康之(電気通信大学大学院)
ページ数 256
サイズ B5変型
ISBN 978-4-7649-0354-8
     
主要目次

第1章 設計モデル検証とモデル検査
1.1 分散システムを開発する際の課題
1.2 ソフトウェア検証とは?

第2章 モデル検査概論
2.1 振る舞いの特性
2.2 モデル検査の仕組み

第3章 モデル検査ツールSPIN概要
3.1 PROMELA/SPIN概要
3.2 PROMELA入門

第4章 SPINによるモデル検査
4.1 モデル検査
4.2 Xspin
4.3 演習問題

第5章 SPINによる設計モデルの検証プロセス
5.1 検証プロセス概論
5.2 検証プロセスの詳細

第6章 設計モデルの検証の実際
6.1 例題:HD/DVDレコーダのネットワーク連携
6.2 検証要求の分析例
6.3 検証対象モデルの設計例
6.4 検証対象モデルの実装例
6.5 検証と設計へのフィードバッグ例
6.6 演習問題

第7章 検証の実践:抽象化・効率化・デバッグ
7.1 パターンを使った性質の記述
7.2 抽象化・スライシング
7.3 検証効率化
7.4 バグの発見・原因追究・修正

付録A PROMELA/SPINリファレンスマニュアル
付録B 設計モデルの検証プロセス
付録C 簡易ステートマシン図のシンタックスとセマンティクス
付録D 簡易ステートマシン図とPROMELAの対応

トップへ
 
本サイトのご利用についてお問合せプライバシーについて | 会社概要 | インプレスグループサイト | インプレスグループTop |
 Copyright © 2016 Kindai kagaku sha Co.,Ltd, an Impress Group company. All rights reserved.