参加者 沼田（読み手）、今井、青木（記）
範囲 pp. 217 – 22４
第10章 ケーススタディ(5) デザイン検証の実際を知る — 分散コンポーネントの振舞い検証
- 10.2 システム記述と検査性質
- 10.2.2 性質の表現と検査の方法
- 21.2.3 振舞い検査
- 10.3 まとめ
- 10.3.1 事例に関する経験のまとめ
p.222 最下行 誤植 誤:「満たされない可能が」、正:「満たされない可能性が」 - 10.3.2 モデル検査法の役割
- 10.3.1 事例に関する経験のまとめ
Monthly Archives: 7月 2011
参加者 青木（読み手）、今井（記）
範囲 pp. 205 – 217
第10章 ケーススタディ(5) デザイン検証の実際を知る — 分散コンポーネントの振舞い検証
- 10.1 ドキュメントからのモデリング
- 10.1.1 検査の対象と作業過程の概要
- 10.1.2 EJBフレームワーク
- 10.2 システム記述と検査性質
- 10.2.1 Promela記述
- p.214 図10.7 do内のremoteからBusinessMethodを受けたときの処理内
retvaFC ? value ->→retvalFC ? value -> - p.216 図10.9
一つの状態から同じイベントの遷移が複数あるところがある(例えばload enabledのreqBM)。実際のシステムではなんらかのガード条件があるが、モデル化（Promelaプロセス記述）したときに「どちらかの遷移が起こる」ということで十分なので、ガードをはずしたということ？
- p.214 図10.7 do内のremoteからBusinessMethodを受けたときの処理内
- 10.2.1 Promela記述
参加者 今井（読み手）、青木（記）
範囲 pp. 195 – 204
第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ — 抽象化の方法
- 9.3 制御の流れに着目した抽象化
- 9.3.3 関連する話題 (p.195 9行目から)
- 9.4 連続時間の抽象化
- 9.4.1 時間オートマトン
- 9.4.2 リージョン・オートマトンの解析
p.201 l.2 「図9.16の状態S0からの３つの遷移は」は「図.9.18の状態S0からの３つの遷移は」の誤りではないでしょうか。
p.201 の「図9.20遷移(その１)」のifブロックのs.regionが非決定的に選択される箇所の「::s.region=R01」は「::s.region=R10」の誤りではないでしょうか。
参加者 青木（読み手）、沼田、今井（記）
範囲 pp. 186 – 195
第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ — 抽象化の方法
- 9.3 制御の流れに着目した抽象化
- 9.3.2 反例の利用
- p.190 図9.12 inline FSMの1行目
LstateAck → LstateAcq - プログラム例の変数名や引数名が1文字だったり短く省略された名前だったりする（例えば図9.14）ので、何を表しているかわかりにくい。普段Javaなどでわかりやすい変数名をつける習慣があるので結構気になる。文化の違い?
- p.190 図9.12 inline FSMの1行目
- 9.3.3 関連する話題 (p.195 8行目まで)
- p.195 2行目行末
変数nの保持する。 → 変数nに保持する。
- p.195 2行目行末
- 9.3.2 反例の利用
参加者 今井（読み手）、青木、沼田（記）
範囲 pp. 176 – 186
第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ — 抽象化の方法
- 9.2 データ値に着目した抽象化
- 9.2.1 カウンタの抽象化
- 図9.3 l.3
actrive → active - p.177 l.6
ℤ：整数 (独: Zahlen)の全体（ウィキペディア 数学記号の表 の 集合論の記号＞特定の集合 より） - 図9.4 inlineの定義の最後
if → fi
- 図9.3 l.3
- 9.2.2 酒屋在庫問題
- 9.2.1 カウンタの抽象化
- 9.3 制御の流れに着目した抽象化
- 9.3.1 述語抽象を用いたモデル検査
参加者 沼田（読み手）、今井、青木（記）
範囲 pp. 165 – 176
第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う — システムソフトウェアへの適用
- 8.2 リアルタイム・スケジューリング
- 8.2.3 解析の実験
p.166 l.4 誤植 誤：「プリオリティ逆転」 正：「プライオリティ逆転」
p.168 図8.26について、勉強会では実行順序が修正したPromela記述と違うように思えたが、実行周期に注意してじっくり考えると正しい。
- 8.2.3 解析の実験
第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ — 抽象化の方法
- 9.1 抽象化の重要性
- 9.1.1 抽象化の役割
- 9.1.2 健全な抽象化
- 9.1.3 アドホックな抽象化
参加者 青木（読み手）、沼田、今井（記）
範囲 pp. 153 – 164
第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う — システムソフトウェアへの適用
- 8.2 リアルタイム・スケジューリング
- 8.2.1 リアルタイムタスクのプライオリティ逆転
- 8.2.2 Promeraを用いた記述
- p. 158 中ほど
advancTick() → advanceTick() - p. 161 図8.18 ifの条件記述
例えば、
(NEXTDEADLINE(I) < tickCount)
は、tickCountが変わる数（主体）でNEXTDEADLINE(I)が比較対象、つまり「tickCountがNEXTDEADLINE(I)より大きいか」という意味なので、
(tickCount > NEXTDEADLINE(I))
の方が読みやすいですね。 - p.163 図8.20
lock(2)やunlock(2)の’2’は何?
→ 図8.21や8.22を見ると、タスクやタスク番号のようだが、なぜ定数2なのだろう。
- p. 158 中ほど