形式的モデル化 - 離散事象／実時間／ハイブリッドシステムのモデル化と

著者名：平石邦彦

森北出版株式会社（2019/01発売）

• ISBN：9784627854215

内容説明

ソフトウェアが正しく設計されているかを保証するための手法として，システムを数学的に厳密なモデルで記述し，仕様が満たされているかどうかを数理的に調べる，「形式検証」が注目されている．

本書では，モデル検査に代表されるように，現実のシステムにも適用可能になってきた形式検証を理解し，使いこなすための理論的背景について解説する．

離散事象，連続状態をもつシステム，およびそれらを併せもつハイブリッドシステムなど，さまざまなシステムに対する形式的モデル化手法と，その解析方法が網羅された1冊．

目次

◆第Ⅰ部　システムのモデル化
第1章　システムの概念
第2章　オートマトンと形式言語
第3章　ペトリネット
第4章　プロセス代数

◆第Ⅱ部　性質・ふるまいの記述
第5章　時相論理によるシステムの性質の記述
第6章　遷移システム・ラベル付き遷移システム

◆第Ⅲ部　拡張モデル
第7章　時間・確率システムのモデル化
第8章　ハイブリッドシステムのモデル化

◆第Ⅳ部　解析・検証・制御
第9章　基本的解析問題
第10章　決定性時間システム・ハイブリッドシステムの解析
第11章　確率システムの解析
第12章　モデル検査
第13章　離散事象システムの制御

付録A　数学用語の解説
付録B　演習問題の解答例

感想・レビュー

※以下の感想・レビューは、株式会社ドワンゴの提供する「読書メーター」によるものです。

[kamocyc]

ハイブリッドシステムのモデル検査はまだニッチな分野だろうし，発展途上でもあると思うが，この本でなんとなく概観はつかんだように思う． ペトリネットやプロセス代数，時相論理など学んだ．

2020/03/07