内容紹介
ソフトウェアの検証、並行性、非決定性を実践的に学べる
モデル検査ツールSPINは、並行分散系のモデル記述および検証に広く用いられている。
本書はSPINを学ぶための優れた入門書の日本語翻訳で、逐次プログラムから並行分散系へと徐々にカリキュラムの難度を上げながらSPINを実際に動かしつつ、モデル記述やSPINを用いた検証を支える考え方や概念まで着実に身に着くもの。
このような方におすすめ
・計算機科学やソフトウェア工学を学ぶ学部学生
・モデル検査に関連する研究を行っている博士課程(前期・後期)の学生
・モデル検査に興味を持つシステム/ソフトウェアエンジニア
目次
主要目次
第1章 PROMELA逐次モデル記述
第2章 逐次モデル記述の検証
第3章 並行性
第4章 同期機構
第5章 時相論理による検証
第6章 データとモデル記述の構造
第7章 通信チャネル
第8章 非決定性
第9章 PROMELAの高度な使い方
第10章 SPINの高度な話題
第11章 ケーススタディ
付録 ソフトウェアツール／リンク集