近代科学社

書籍検索
ジャンル選択

情報

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

並行システムの検証と実装形式手法CSPに基づく高信頼並行システム開発入門

監修　東野 輝夫
著者　磯部 祥尚

著者紹介

並行システムとは、マルチコアCPUを備えるPCやスマホのほか、組込み、スマートグリッドの処理にも欠かせないシステムである。本書は、その基礎理論（プロセス代数）であるCSPを用いた並行システムの構築方法や検証、実装の方法を概説。ソフトウェア開発者を中心に、並行プログラミングに挑戦したい人への一冊。

電子書籍¥5,060 小売希望価格（税込）

紙の書籍¥5,060定価（税込）

基本情報

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

主要目次

第1章CSP,FDR,JCSP概論
　1.1CSP,FDR,JCSPの紹介
　1.2CSP,FDR,JCSPの効果
　1.3並行システムの検証例／実装例
　1.4まとめ
　1.5演習問題

第2章CSP入門
　2.1基本演算子
　2.2複製型演算子
　2.3変数と送受信
　2.4並行合成とチャネル
　2.5CSPモデルの例（食事する哲学者）
　2.6もう1つの並行合成演算子
　2.7まとめ2.8演習問題

第3章FDR入門
　3.1モデル検査
　3.2構文
　3.3FDR使用法
　3.4まとめ
　3.5演習問題

第4章JCSP入門
　4.1CSPライブラリ
　4.2チャネル
　4.3プロセス
　4.4食事する哲学者の実装
　4.5まとめ
　4.6演習問題

第5章CSP理論（動作表現）
　5.1並行システムの状態遷移図の例
　5.2状態遷移図
　5.3遷移規則
　5.4状態遷移図表示ツールProBE
　5.5まとめ
　5.6演習問題

第6章CSP理論（動作解析）
　6.1CSPモデルの動作解析
　6.2トレース方式
　6.3安定失敗方式
　6.4失敗発散方式
　6.5詳細化の例
　6.6CSPの基礎
　6.7まとめ
　6.8演習問題

第7章FDR検証
　7.1詳細化関係検証ツールFDR
　7.2詳細化関係による検証例
　7.3抽象化による検証例
　7.4匿名性の検証例
　7.5まとめ
　7.6演習問題

第8章JCSP実装
　8.1共用チャネル
　8.2ネットワークチャネル
　8.3GUI
　8.4まとめ
　8.5演習問題

第9章CSP,FDR,JCSP応用
　9.1チャネル渡し
　9.2送受信待ちの取消
　9.3まとめ

第10章CSP,FDR,JCSP実践
　10.1CSPによるモデル化
　10.2FDRによる検証
　10.3JCSPによる実装
　10.4まとめ

付録Aインストール方法
　A.1JCSP（Javaライブラリ）
　A.2FDR（モデル検査器）
　A.3TypeChecker（型検査器）
　A.4ProBE（状態遷移表示器）

付録B演習問題解答
　B.1第1章演習問題（1.5節，p.29）解答
　B.2第2章演習問題（2.8節，p.76）解答
　B.3第3章演習問題（3.5節，p.108）解答
　B.4第4章演習問題（4.6節，p.146）解答
　B.5第5章演習問題（5.6節，p.179）解答
　B.6第6章演習問題（6.8節，p.225）解答
　B.7第7章演習問題（7.6節，p.254）解答
　B.8第8章演習問題（8.5節，p.281）解答

参考文献
索引

目次をさらに表示する

著者紹介

シリーズ監修者
本位田　真一（ほんいでん　しんいち）
1978 年　早稲田大学大学院理工学研究科博士前期課程　修了
1978 年　株式会社　東芝
現　在　　国立情報学研究所教授・東京大学大学院情報理工学系研究科教授　工学博士

監修者・著者紹介（※は監修者）

東野　輝夫（ひがしの　てるお）（※）
1984 年　大阪大学大学院基礎工学研究科博士後期課程修了　工学博士
1984 年　大阪大学　助手
現　在　　大阪大学大学院情報科学研究科　教授
並行分散システム、モバイル・コンピューティングなどに関する研究に従事。

磯部　祥尚（いそべ　よしなお）
1992 年　芝浦工業大学大学院電気工学専攻修士課程　修了
1992 年　通商産業省工業技術院電子技術総合研究所
現　在　　独立行政法人産業技術総合研究所主任研究員・北陸先端科学技術大学院大学客員　准教授　工学博士
形式手法による並行システムの検証に関する研究に従事。

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