近代科学社

書籍検索
ジャンル選択

情報

トップエスイー実践講座 第3巻

SPINによる設計モデル検証モデル検査の実践ソフトウェア検証

監修 萩谷 昌己
著者 吉岡 信和
著者 青木 利晃

著者紹介

昨今、ソフトウェアの正しさを保証するソフトウェア検証の技術が重要視されているが、その中でも特にモデル検査が脚光を浴びている。それは数理論理学などに関する知識があまりない技術者にも、ソフトウェア開発の中で利用することが可能だからであろう。本書はSPINを中心にモデル検査をいかにしてソフトウェア開発のプロセスの中に位置づけるかについて実例を通して詳説している。

電子書籍¥3,960 小売希望価格(税込)

紙の書籍¥3,960定価(税込)

基本情報

発売日 2008年9月26日
本体価格 3,600円
ページ数 256 ページ ※印刷物
サイズ B5 変形
ISBN 9784764903548
ジャンル 情報
タグ ソフトウェア工学
電子書籍形式 固定型

主要目次

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

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

第 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 検証対象モデル(VM)の実装例
6.5 検証と設計へのフィードバッグ例
6.6 演習問題

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

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

目次をさらに表示する

著者紹介

シリーズ監修者

本位田 真一(ほんいでん しんいち)
1978 年 早稲田大学大学院理工学研究科博士前期課程修了
1978 年 株式会社東芝
国立情報学研究所教授・東京大学大学院情報理工学系研究科教授 工学博士

監修者・著者紹介(※は監修者)

萩谷 昌己(はぎや まさみ)(※)
1982 年 東京大学大学院理学系研究科修士課程修了
東京大学大学院情報理工学系研究科教授 理学博士
形式的手法,理論計算機科学の研究に従事。
計算モデル、形式的検証、プログラミング言語、分子コンピューティングに興味を持つ。

吉岡 信和(よしおか のぶかず)
1998 年 北陸先端科学技術大学院大学情報科学研究科博士後期課程修了
1998 年 株式会社東芝
国立情報学研究所准教授・総合研究大学院大学准教授 博士(情報科学)
ソフトウェア工学、形式手法、セキュリティソフトウェア工学、セキュリティパターンの研究・教育に従事。

青木 利晃(あおき としあき)
1999 年 北陸先端科学技術大学院大学情報科学研究科博士後期課程修了
北陸先端科学技術大学院大学安心電子社会研究センター特任准教授 博士(情報科学)
ソフトウェア工学・科学、形式手法、形式検証の研究に従事。
オブジェクト指向開発、組込みシステム開発に興味を持つ。

田原 康之(たはら やすゆき)
1991 年 東京大学大学院理学系研究科修士課程修了
1991 年 株式会社東芝
2003 年 国立情報学研究所
電気通信大学大学院情報システム学研究科准教授 博士(情報科学)
エージェント技術、ソフトウェア工学の研究に従事。
特に、エージェント指向開発方法論、モデル検査技術、および要求分析技術に興味を持つ。

著者紹介をさらに表示する