試験公開中

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

ソフトウェア科学基礎:最先端のソフトウェア開発に求められる数理的基礎(トップエスイー基礎講座1)

近代科学社

4,180円 2,090円 (1,900円+税) 《特価》

本書では、優れた開発者として最先端の理論やツールと使ってソフトウェア開発をするために必要な基礎知識である、論理学、並行システム、オートマトン、モデル検査のアルゴリズムや実装技術、モデル検証ツールをまとめて解説する。

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

関連サイト

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

内容紹介

オープンソースの広がりにより、多様な機能を実現することは以前と比較すると驚くばかりに容易になっている。しかし、このような開発法ではスケーラビリティと高信頼性を同時に保証することはできない。機能の実現や追加が比較的安易にできる時代になったからこそ、成長し続けるシステム全体の正常な動作を保証しうる開発検査手法の必要性が増している。 本書では、優れた開発者として最先端の理論やツールと使ってソフトウェア開発をするために必要な基礎知識である、論理学、並行システム、オートマトン、モデル検査のアルゴリズムや実装技術、モデル検証ツールをまとめて解説する。

書誌情報

  • 著者: 本位田 真一, 田中 譲(監修), 磯部 祥尚, 粂野 文洋, 櫻庭 健年, 田口 研治(著)
  • 発行日: (紙書籍版発行日: 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 年 スウェーデン王国ウプサラ大学計算機科学博士号
現在 国立情報学研究所特任教授
形式手法の研究と教育に従事.現在は,安全要求工学,形式仕様とテスティングに興味を持つ.

目次

第0章 これから技術者をめざすひとのために

第1章 論理―正しいと考えられる事柄から正しい事柄を新たに導く

第2章 集合―多様な構造や構成の方法を知る

第3章 並行プログラム―並行性に特有の概念と知識を学ぶ

第4章 時相論理―システムやプログラムの動的な性質を記述する

第5章 検証性質の記述―一般の技術者がシステムの性質を記述する

第6章 オートマトン―コンピュータの動作を形式的に表現する

第7章 モデル検査基礎―並行システムのモデル検査を行う

第8章 モデル検査実装―検証モデル記述のノウハウを利用する

第9章 抽象解釈―モデル検査の複雑さを軽減する

第10章 モデル検査ツール―SPIN,SMV,LTSA,UPPAALを使う

Home 書籍一覧 ソフトウェア科学基礎:最先端のソフトウェア開発に求められる数理的基礎(トップエスイー基礎講座1) ▲ ページトップへ戻る