出版社内容情報
ソフトウェアの形式検証を理解し,使いこなすための理論を詳説.様々なシステムに対する形式的モデル化・解析手法を網羅.ソフトウェアが正しく設計されているかを保証するための手法として,システムを数学的に厳密なモデルで記述し,仕様が満たされているかどうかを数理的に調べる,「形式検証」が注目されている.
本書では,モデル検査に代表されるように,現実のシステムにも適用可能になってきた形式検証を理解し,使いこなすための理論的背景について解説する.
離散事象システム,実時間システム,ハイブリッドシステムなど,さまざまなシステムに対する形式的モデル化手法と,その解析方法が網羅された1冊.
◆第?部 システムのモデル化
第1章 システムの概念
第2章 オートマトンと形式言語
第3章 ペトリネット
第4章 プロセス代数
◆第?部 性質・ふるまいの記述
第5章 時相論理によるシステムの性質の記述
第6章 遷移システム・ラベル付き遷移システム
◆第?部 拡張モデル
第7章 時間・確率システムのモデル化
第8章 ハイブリッドシステムのモデル化
◆第?部 解析・検証・制御
第9章 基本的解析問題
第10章 決定性時間システム・ハイブリッドシステムの解析
第11章 確率システムの解析
第12章 モデル検査
第13章 離散事象システムの制御
付録A 数学用語の解説
付録B 演習問題の解答例
平石 邦彦[ヒライシ クニヒコ]
著・文・その他
内容説明
複雑・多様化するシステムの形式検証のために。堅牢なシステム構築のための、システムの数理的なモデル化・解析手法の理論的背景を詳説。
目次
第1部 システムのモデル化(システムの概念;オートマトンと形式言語 ほか)
第2部 性質・ふるまいの記述(時相論理によるシステムの性質の記述;遷移システム・ラベル付き遷移システム)
第3部 拡張モデル(時間・確率システムのモデル化;ハイブリッドシステムのモデル化)
第4部 解析・検証・制御(基本的解析問題;決定性時間システム・ハイブリッドシステムの解析 ほか)
著者等紹介
平石邦彦[ヒライシクニヒコ]
1983年東京工業大学工学部制御工学科卒業。1985年東京工業大学理工学研究科制御工学専攻修了。富士通(株)国際情報社会科学研究所研究員。1993年北陸先端科学技術大学院大学情報科学研究科助教授。2003年同教授。2016年同大学情報社会基盤研究センター長。工学博士(本データはこの書籍が刊行された当時に掲載されていたものです)
※書籍に掲載されている著者及び編者、訳者、監修者、イラストレーターなどの紹介情報です。