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


株式会社 近代科学社

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

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

book

発売日:2008.09.26
定価:本体3,800円+税

アマゾンで注文

 

形式仕様記述とモデル検査の基礎知識を一気に習得!!

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

 
著者 シリーズ監修:本位田 真一、監修:田中 譲(北海道大学大学院)、磯部 文洋(産業技術総合研究所)、粂野 文洋(三菱総合研究所)櫻庭 健年(日立システム開発研究所)、田口 研治(国立情報学研究所)、田原 康之(電気通信大学大学院)
ページ数 384
サイズ B5変型
ISBN 978-4-7649-0355-5
     
主要目次

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

第2章 集合―多様な構造や構成の方法を知る
集合と元
包含関係
集合の演算
集合算の法則
集合族
関数,写像
集合の同等性
公理的集合論
列上の帰納法
バグ(bag)

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

第4章 時相論理―システムやプログラムの動的な性質を記述する
命題線形時相論理PLTL
分岐時相論理CTL

第5章 検証性質の記述―一般の技術者がシステムの性質を記述する
到達可能性
安全性
活性
公平性
性質記述パターン

第6章 オートマトン―コンピュータの動作を形式的に表現する
有限オートマトン
正規表現
B¨uchiオートマトン
時間オートマトン

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

第8章 モデル検査実装―検証モデル記述のノウハウを利用する
BDD(二分決定グラフ)による記号モデル検査
部分順序関係を利用した状態数削減
On-the-fly手法
ハッシュ手法
状態圧縮

第9章 抽象解釈―モデル検査の複雑さを軽減する
抽象化とは
データ抽象
述語抽象
抽象化と健全性
プログラムスライシング

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

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