著者・出版社・関連アーティスト
商品説明
リソースには限界がある。技術者にとって大切なことは制約の中で目的とする記述を得る方法の習得である。本書はまさにこのようなモデリング技法について述べている。
関連記事
収録内容
| 1 | 第1章 モデル検査とは-自動検証とモデル検査法 |
| 2 | 第2章 SPINを使ってみよう-Promelaの書き方とコマンドの使い方 |
| 3 | 第3章 性質を表現する-正しさの基準 |
| 4 | 第4章 対象を広げる-Promelaの実行規則 |
| 5 | 第5章 仕組みを理解する-SPINの検証法 |
| 6 | 第6章 ケーススタディ・1ソフトウェアデザインを検証する-状態遷移ダイアグラムの解析 |
| 7 | 第7章 ケーススタディ・2モデル検査を使い分ける-Java並行プログラムの解析 |
| 8 | 第8章 ケーススタディ・3組込みソフトウェアの解析に使う-システムソフトウェアへの適用 |
| 9 | 第9章 ケーススタディ・4検査対象の大きさを適切に保つ-抽象化の方法 |
| 10 | 第10章 ケーススタディ・5デザイン検証の実際を知る-分散コンポーネントの振舞い検証 |
