試験公開中

このエントリーをはてなブックマークに追加

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

近代科学社

3,600円+税

本書はSPINを中心にモデル検査をいかにしてソフトウェア開発のプロセスの中に位置づけるかについて実例を通して詳説している。

【注意】本書のEPUB版は固定レイアウト型になっております。文字の大きさの変更や検索、引用などはお使いいただけません。画面の大きい端末でご利用ください。

関連サイト

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

内容紹介

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

書誌情報

  • 著者: 本位田 真一, 萩谷 昌己(監修), 吉岡 信和, 青木 利晃, 田原 康之(著)
  • 発行日: (紙書籍版発行日: 2008-09-30)
  • 最終更新日: 2018-03-23
  • バージョン: 1.0.0
  • ページ数: 251ページ(PDF版換算)
  • 対応フォーマット: PDF, EPUB
  • 出版社: 近代科学社

対象読者

設計モデル検証,モデル検査,SPIN,PROMELAに興味がある人

著者について

本位田 真一

1978年 早稲田大学大学院理工学研究科博士前期課程 修了
1978年 株式会社 東芝
現 在 国立情報学研究所 教授・東京大学大学院情報理工学系研究科 教授 工学博士

萩谷 昌己

1982 年 東京大学大学院理学系研究科修士課程修了
現在 東京大学大学院情報理工学系研究科教授 理学博士
形式的手法,理論計算機科学の研究に従事.計算モデル,形式的検証,プログラミング言語,分子コンピューティングに興味を持つ.

吉岡 信和

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

青木 利晃

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

田原 康之

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

目次

第1章 設計モデル検証とモデル検査

第2章 モデル検査概論

第3章 モデル検査ツールSPIN概要

第4章 SPINによるモデル検査

第5章 SPINによる設計モデルの検証プロセス

第6章 設計モデルの検証の実際

第7章 検証の実践:抽象化・効率化・デバッグ

付録A PROMELA/SPINリファレンスマニュアル

付録B 設計モデルの検証プロセス

付録C 簡易ステートマシン図のシンタックスとセマンティクス

付録D 簡易ステートマシン図とPROMELAの対応

Home 書籍一覧 SPINによる設計モデル検証:モデル検査の実践ソフトウェア検証(トップエスイー実践講座3) ▲ ページトップへ戻る