関連サイト
本書の関連ページが用意されています。
内容紹介
昨今、ソフトウェアの正しさを保証するソフトウェア検証の技術が重要視されているが、その中でも特にモデル検査が脚光を浴びている。それは数理論理学などに関する知識があまりない技術者にも、ソフトウェア開発の中で利用することが可能だからであろう。本書はSPINを中心にモデル検査をいかにしてソフトウェア開発のプロセスの中に位置づけるかについて実例を通して詳説している。
書誌情報
- 著者: 本位田 真一, 萩谷 昌己(監修), 吉岡 信和, 青木 利晃, 田原 康之(著)
- 発行日: 2018-03-23 (紙書籍版発行日: 2008-09-30)
- 最終更新日: 2018-03-23
- バージョン: 1.0.0
- ページ数: 251ページ(PDF版換算)
- 対応フォーマット: PDF, EPUB
- 出版社: 近代科学社
対象読者
設計モデル検証,モデル検査,SPIN,PROMELAに興味がある人
著者について
本位田 真一
1978年 早稲田大学大学院理工学研究科博士前期課程 修了
1978年 株式会社 東芝
現 在 国立情報学研究所 教授・東京大学大学院情報理工学系研究科 教授 工学博士
萩谷 昌己
1982 年 東京大学大学院理学系研究科修士課程修了
現在 東京大学大学院情報理工学系研究科教授 理学博士
形式的手法，理論計算機科学の研究に従事．計算モデル，形式的検証，プログラミング言語，分子コンピューティングに興味を持つ．
吉岡 信和
1998 年 北陸先端科学技術大学院大学情報科学研究科博士後期課程修了
1998年 株式会社東芝
現在 国立情報学研究所准教授・総合研究大学院大学准教授 博士（情報科学）
ソフトウェア工学，形式手法，セキュリティソフトウェア工学，セキュリティパターンの研究・教育に従事．
青木 利晃
1999 年 北陸先端科学技術大学院大学情報科学研究科博士後期課程修了
現在 北陸先端科学技術大学院大学安心電子社会研究センター特任准教授 博士（情報科学）
ソフトウェア工学・科学，形式手法，形式検証の研究に従事．オブジェクト指向開発，組込みシステム開発に興味を持つ．
田原 康之
1991 年 東京大学大学院理学系研究科修士課程修了
1991年 株式会社東芝
2003年 国立情報学研究所
現在 電気通信大学大学院情報システム学研究科准教授 博士（情報科学）
エージェント技術，ソフトウェア工学の研究に従事．特に，エージェント指向開発方法論，モデル検査技術，および要求分析技術に興味を持つ．