Monthly Archives: 7月 2011

「SPINモデル検査」第22回(7月26日)

Posted on by 0 comment

参加者 沼田(読み手)、今井、青木(記)
範囲 pp. 217 – 224

第10章 ケーススタディ(5) デザイン検証の実際を知る — 分散コンポーネントの振舞い検証

  • 10.2 システム記述と検査性質
    • 10.2.2 性質の表現と検査の方法
    • 21.2.3 振舞い検査
  • 10.3 まとめ
    • 10.3.1 事例に関する経験のまとめ
      p.222 最下行 誤植 誤:「満たされない可能が」、正:「満たされない可能性が」
    • 10.3.2 モデル検査法の役割

「SPINモデル検査」第21回(7月22日)

Posted on by 0 comment

参加者 青木(読み手)、今井(記)
範囲 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プロセス記述)したときに「どちらかの遷移が起こる」ということで十分なので、ガードをはずしたということ?

「SPINモデル検査」第20回(7月19日)

Posted on by 0 comment

参加者 今井(読み手)、青木(記)
範囲 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からの3つの遷移は」は「図.9.18の状態S0からの3つの遷移は」の誤りではないでしょうか。
      p.201 の「図9.20遷移(その1)」のifブロックのs.regionが非決定的に選択される箇所の「::s.region=R01」は「::s.region=R10」の誤りではないでしょうか。

「SPINモデル検査」第19回(7月15日)

Posted on by 0 comment

参加者 青木(読み手)、沼田、今井(記)
範囲 pp. 186 – 195

第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ — 抽象化の方法

  • 9.3 制御の流れに着目した抽象化
    • 9.3.2 反例の利用
      • p.190 図9.12 inline FSMの1行目
        LstateAck → LstateAcq
      • プログラム例の変数名や引数名が1文字だったり短く省略された名前だったりする(例えば図9.14)ので、何を表しているかわかりにくい。普段Javaなどでわかりやすい変数名をつける習慣があるので結構気になる。文化の違い?
    • 9.3.3 関連する話題 (p.195 8行目まで)
      • p.195 2行目行末
        変数nの保持する。 → 変数n保持する。

「SPINモデル検査」第18回(7月12日)

Posted on by 0 comment

参加者 今井(読み手)、青木、沼田(記)
範囲 pp. 176 – 186

第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ — 抽象化の方法

「SPINモデル検査」第17回(7月8日)

Posted on by 0 comment

参加者 沼田(読み手)、今井、青木(記)
範囲 pp. 165 – 176

第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う — システムソフトウェアへの適用

  • 8.2 リアルタイム・スケジューリング
    • 8.2.3 解析の実験
      p.166 l.4 誤植 誤:「プリオリティ逆転」 正:「プライオリティ逆転」
      p.168 図8.26について、勉強会では実行順序が修正したPromela記述と違うように思えたが、実行周期に注意してじっくり考えると正しい。

第9章 ケーススタディ(4) 検査対象の大きさを適切に保つ — 抽象化の方法

  • 9.1 抽象化の重要性
    • 9.1.1 抽象化の役割
    • 9.1.2 健全な抽象化
    • 9.1.3 アドホックな抽象化

「SPINモデル検査」第16回(7月5日)

Posted on by 0 comment

参加者 青木(読み手)、沼田、今井(記)
範囲 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なのだろう。