関連サイト
本書の関連ページが用意されています。
内容紹介
オープンソースの広がりにより、多様な機能を実現することは以前と比較すると驚くばかりに容易になっている。しかし、このような開発法ではスケーラビリティと高信頼性を同時に保証することはできない。機能の実現や追加が比較的安易にできる時代になったからこそ、成長し続けるシステム全体の正常な動作を保証しうる開発検査手法の必要性が増している。 本書では、優れた開発者として最先端の理論やツールと使ってソフトウェア開発をするために必要な基礎知識である、論理学、並行システム、オートマトン、モデル検査のアルゴリズムや実装技術、モデル検証ツールをまとめて解説する。
書誌情報
- 著者: 本位田 真一, 田中 譲(監修), 磯部 祥尚, 粂野 文洋, 櫻庭 健年, 田口 研治(著)
- 発行日: 2018-03-23 (紙書籍版発行日: 2009-05-31)
- 最終更新日: 2018-03-23
- バージョン: 1.0.0
- ページ数: 365ページ(PDF版換算)
- 対応フォーマット: PDF, EPUB
- 出版社: 近代科学社
対象読者
ソフトウェア,論理,集合,並行プログラム,時相論理,検証性質,オートマトン,モデル検査,並行システム,検証モデル記述,抽象解釈,SPIN,SMV,LTSA,UPPAALに興味がある人
著者について
本位田 真一
1978年 早稲田大学大学院理工学研究科博士前期課程 修了
1978年 株式会社 東芝
現 在 国立情報学研究所 教授・東京大学大学院情報理工学系研究科 教授 工学博士
田中 譲
1974 年 京都大学大学院工学研究科修士課程修了
現在 北海道大学大学院情報科学研究科教授 工学博士
知識メディア，知識連携の研究に従事．
磯部 祥尚
1992 年 芝浦工業大学大学院電気工学専攻修士課程修了
1992 年 通商産業省工業技術院電子技術総合研究所
現在 独立行政法人産業技術総合研究所主任研究員・国立情報学研究所特任准教授 工学博士
形式手法による並行システムの検証に関する研究に従事．
粂野 文洋
1990 年 早稲田大学大学院理工学研究科数学専攻修士課程修了
株式会社三菱総合研究所情報技術研究センター主任研究員・国立情報学研究所特任准教授
自動推論，エージェント技術，自己適応型ソフトウェアアーキテクチャ，形式手法ツールの応用等に興味を持つ．
櫻庭 健年
1983 年 東北大学大学院博士課程数学専攻前期課程修了
1983 年 株式会社日立製作所
現在 株式会社日立製作所システム開発研究所
オペレーティングシステム，情報セキュリティの研究に従事．情報プラットフォームのセキュリティ機能に興味を持つ．
田口 研治
2001 年 スウェーデン王国ウプサラ大学計算機科学博士号
現在 国立情報学研究所特任教授
形式手法の研究と教育に従事．現在は，安全要求工学，形式仕様とテスティングに興味を持つ．