TOP > 情報工学
 □ ニュースリリース
コミュニケーション・
情報リテラシー
工学一般
情報工学
電子工学
数学
物理学
ビジネス・経済
建築・都市計画
科学一般
公立はこだて未来大学出版会
発行
ナノオプト発行
弊社の書籍はお近くの書店・大学生協でお求めいただけます。店頭にない場合はお店からお取り寄せもできます。また、インターネットでもご購入いただけますので各販売サイトをご覧ください。
  サポート
   正誤表、授業用の教材などが
   あります
  地図(インプレスグループ)
   Google Map


株式会社 近代科学社

〒162-0843
東京都新宿区市谷田町2-7-15
TEL : 03-3260-6161
FAX : 03-3260-6059

 
情報工学
 
トップエスイー実践講座1 ソフトウェアシステムのモデル化とその検証
Bメソッドによる形式仕様記述

book

発売日:2007.12.27
定価:本体3,600円+税

アマゾンで注文

 

「日本初!待望のBメソッド解説書!!」仕様の段階で誤りをなくす注目の手法「Bメソッド」を実践活用するための解説書!

安心安全を含めてますます高度な機能や性能が要求されるソフトウェアシステムの開発において、厳密な仕様記述を基に開発を行う形式手法に対する関心と期待が高まる中で、我が国初のBメソッドの書き下ろし入門書が出版されました。実際の開発への適用を意識した実用指向の内容を平明でわかりやすく記述した本書を、形式手法の理解と習得に格好の書として推薦いたします。荒木啓二郎・九州大学大学院システム情報科学研究院教授

 
著者 監修:中島 震(国立情報学研究所)
著者:来間 啓伸(日立製作所 システム開発研究所)
ページ数 240
サイズ B5変型
ISBN 978-4-7649-0347-0
     
主要目次

第1章 形式手法概論
1.1 ソフトウェア開発過程
1.2 形式手法
1.3 B メソッド

第2章 形式仕様の作成
2.1 形式仕様
2.2 算術演算を使う例題―ポイント計算
2.3 抽象機械の書き方
2.4 抽象機械の整合性の検証
2.5 ツールを使った整合性の検証
2.6 演習問題

第3章 抽象機械
3.1 集合と関係を使う例題―座席予約
3.2 抽象機械の記法
3.3 抽象機械の構造化
3.4 抽象機械の整合性検証
3.5 ツールを使った整合性の検証
3.6 型チェック
3.7 抽象機械における事前条件の意味
3.8 演習問題

第4章 仕様から実装へのステップ
4.1 仕様の段階的詳細化
4.2 開発過程で使われる記述

第5章 リファインメント
5.1 データ詳細化の例題―有向グラフ
5.2 リファインメントの記法
5.3 詳細化の正当性検証
5.4 ツールを使った整合性と正当性の検証
5.5 リファインメントにおける事前条件の意味
5.6 演習問題

第6章 インプリメンテーション
6.1 実装段階のための例題―座席予約
6.2 インプリメンテーションの記法
6.3 ライブラリ
6.4 詳細化の正当性検証
6.5 ツールを使った整合性と正当性の検証
6.6 輸入における事前条件の役割
6.7 演習問題

第7章 事例研究
7.1 アドホックネットワーク
7.2 題材の概要
7.3 モデル化の方針
7.4 モデル1
7.5 モデル2

第8章 次のステップ
8.1 B メソッドのまとめ
8.2 Event-B

解答、B言語の記号、Bによる事例研究の記述

トップへ
 
本サイトのご利用についてお問合せプライバシーについて | 会社概要 | インプレスグループサイト | インプレスグループTop |
 Copyright © 2016 Kindai kagaku sha Co.,Ltd, an Impress Group company. All rights reserved.