SPIN モデル検査: 検証モデリング技法近代科学社, 1899/12/30 - 238 ページ SPINの基礎から実際の利用方法までを具体的に解説する日本で ◆SPINとは？ 社会の様々なところにソフトウェアが組み込まれ、 そのテスト手法に代わるものとして注目されてきているのが形式的 【目次】 第1章 モデル検査とは?自動検証とモデル検査法 第2章 SPINを使ってみよう? 第3章 性質を表現する?正しさの基準 第4章 対象を広げる?Promelaの実行規則 第5章 仕組みを理解する?SPINの検証法 第6章 ケーススタディ(1) ソフトウェアデザインを検証する?状態遷移ダイアグラムの解析 第7章 ケーススタディ(2) モデル検査を使い分ける?Java並行プログラムの解析 第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う?システムソフトウェアへの適用 第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ?抽象化の方法 第10章 ケーススタディ(5) デザイン検証の実際を知る?分散コンポーネントの振舞い検証 |
目次
第2章 SPINを使ってみようPromelaの書き方とコマンドの使い方 | 15 |
第3章性質を表現する正しさの基準 | 33 |
第4章対象を広げるPromelaの実行規則 | 57 |
第5章仕組みを理解するSPINの検証法 | 73 |
第6章ケーススタディ1 ソフトウェアデザインを検証する状態遷移ダイアグラムの解析 | 97 |
第7章ケーススタディ2 モデル検査を使い分けるJava並行プログラムの解析 | 129 |
第8章ケーススタディ3 組込みソフトウェアの解析に使うシステムソフトウェアへの適用 | 147 |
第9章ケーススタディ4 検査対象の大きさを適切に保つ抽象化の方法 | 171 |
他の版 - すべて表示
多く使われている語句
_lock(OBJ _pid _unlock(OBJ a.exe active proctype assert(false atomic B¨uchi bigN BigX bool byte change[I].state change[I].togo clearSpeed Client cName CruiseController currentEV disableControl E.M. Clarke ejbActivate ejbLoad EJBObject ejbPassivate ejbRemove ejbStore emptyValue enableControl engineOff engineOn Enterprise JavaBeans Entity Bean ERROR ErrorNotify false fullValue G.J. Holzmann gcc pan.c goto accept_S4 goto Inactive GstateLocked H_state inline INTR Java L(Mf lock low_priority Mars PathFinder Mealy Model Checker mthd mtype mutex NBUF notify notifyAll nPackets nPacketsOld Order Reduction Partial Order Reduction printf Promela Promela/SPIN recordSpeed running s.region Sender skip smallN software SPIN SPIN Model Checker StartButton stateC stateLamp stock StopButton synchronized T0_init taskRun throws InterruptException tickCount timeout to_rcvr to_sndr toControl toCruise toHW toSakaya toSpeed toStateM true turn typedef unlock void waiting あるいは オートマトン ガード つの である では と図 ならびに に示した プロセス プロセス名 引数 文の列 次に、図 記述