Monthly Archives: 3月 2011

「SPINモデル検査入門」第13回(3月29日)

Posted on by 0 comment

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

第7章 通信チャネル

  • 7.6 ソート機能付き送信
  • 7.7 メッセージのコピー
  • 7.8 ポーリング
  • 7.9 ランデブとバッファ付き通信チャネルの比較
    • p.139 下から4行目 行頭 脱字
      バファ付き → バファ付き

第8章 非決定性

  • 8.1 非決定性有限オートマトン
    • p.143 ソースコード8.1
      hを0に初期化はしなくて良いか?

      全ての変数は初期値が0に設定されることになっているが、変数の宣言時に明示的に初期値を設定するほうがよい。(p.5 [注意]より)

    • 8.1.1 timeout
    • 8.1.2 検証による受理過程の発見
    • 8.1.3 すべての判例の検出
    • 8.1.4 λ-遷移
  • 8.2 VN:非決定性の視覚化ツール
    • p.148 Findのl.3
      「証左」の意味は?

      事実を明らかにするよりどころとなるもの。証拠。(「大辞泉」より)

「SPINモデル検査入門」第12回(3月25日)

Posted on by 0 comment

参加者 今井(読み手)、青木(記)
範囲 pp. 122 – 135

第7章 通信チャネル

  • 7.2 ランデブ通信チャネル
    p.122 l.16 「3つのプロセス」のあとに「は」があるほうが良いと思いました。

    • 7.2.1 応答通信チャネル
      p.125 l.7 「応答を受信したクライアント」のあとの「は」は不要。「(11行目)」は「(18行目)」の誤り。
    • 7.2.2 通信チャネルの配列
    • 7.2.3 局所チャネル
    • 7.2.4 ランデブ通信チャネルの制限
  • 7.3 バッファ付き通信チャネル
  • 7.4 通信チャネルの状態確認
    • 7.4.1 通信チャネルの一杯と空のチェック
    • 7.4.2 通信チャネルの中のメッセージを数える
  • 7.5 ランダム受信

「SPINモデル検査入門」第11回(3月22日)

Posted on by 0 comment

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

第6章 データとモデル記述の構造

  • 6.2 タイプ定義
  • 6.3 プリプロセッサ
    • 6.3.1 条件付きコンパイル
    • 6.3.2 マクロ
  • 6.4 インライン展開

第7章 通信チャネル

  • 7.1 Promelaの通信チャネル
    • 7.1.1 通信チャネルと通信チャネル変数

「SPINモデル検査入門」第10回(3月18日)

Posted on by 0 comment

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

第5章 時相論理による検証

  • 5.9 時相論理の高度な使い方
    • 5.9.2 際限なく頻繁に
    • 5.9.3 先行性
    • 5.9.4 追い越し
    • 5.9.5 この次

第6章 データとモデル記述の構造

  • 6.1 配列

「SPINモデル検査入門」第9回(3月11日)

Posted on by 0 comment

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

第5章 時相論理による検証

  • 5.4 活性
    • 5.4.2 Spinによる活性の検証
      • p.93
        l4. wantQが0、wantPが1では?
        START OF CYCLEから下はwantQとwantPが逆?
  • 5.5 公平性
  • 5.6 双対性
    • 双対:そうつい
  • 5.7 ゴースト変数を用いない正当性の検証
    • p.97 ページ中程のコード1行目のmutexの定義はmutexの後ろにスペースが必要では?
  • 5.8 非保護領域のモデル化
  • 5.9 時相論理の高度な使い方
    • 5.9.1 ラッチ
      • p.101 l.9 †10の後ろに句点がいる?

「SPINモデル検査入門」第8回(3月8日)

Posted on by 0 comment

参加者 沼田(読み手)、今井(記)
範囲 pp. 80 – 90

第5章 時相論理による検証

  • 5.2 線形時間理論とは
    • 5.2.2 LTLの意味論
      • p.82 図5.1のキャプション「3番目の状態遷移図」とはどういう意味?
  • 5.3 安全性
    • 5.3.1 LTLによる安全性の表現
    • 5.3.2 Promelaによる安全性の記述
    • 5.3.3 Spinによる安全性の検証
  • 5.4 活性
    • 5.4.1 Spinによる活性の表現

「SPINモデル検査入門」第7回(3月4日)

Posted on by 0 comment

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

第4章 同期機構

  • 4.6 並行システムモデルの非決定性
    • 4.6.1 値の非決定的生成
    • 4.6.2 範囲に属する値の生成
  • 4.7 プロセスの終了停止
    • 4.7.1 デッドロック
      • p.71 l.11 行頭 誤植?
        検証を行うと、 → 検証を行うと、
    • 4.7.2 End状態
      • p.73 l.5 行末 誤植?
        明示すことができる. → 明示すことができる.
    • 4.7.3 プロセス群の終了順序
      • p.75 l.下から6 誤植?
        サーバープロセスクライアントの後に →
        サーバープロセスクライアントの後に

第5章 時相論理による検証

  • 5.1 表明を超えて
  • 5.2 線形時間論理とは
    • 5.2.1 LTLの構文
      • 時相演算子は今までなじみが無いので、ちょっとわかりにくいね。時相演算子を含んだ論理式は、まず時相演算子を無視して解釈し、そこに時相演算子の意味を付け加えて解釈すればわかりやすそう。

「SPINモデル検査入門」第6回(3月1日)

Posted on by 0 comment

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

第4章 同期機構

  • 4.2 文の実行性
    • ソースコードに出てくる::(例えばソースコード4.2のl.5やl.15)はどのような意味?
  • 4.3 状態遷移ダイアグラム
    • l.9 の(6. wantP=0, 13. wantQ=0, x, y)は図4.1の状態のことだろう
  • 4.4 複数文の不可分実行
    • 4.4.1 d_stepとatomic
      • skip:何もしないダミーの文
      • チャネルの構文は7章で出てくるだろう
  • 4.5 セマフォ
  • 4.6 並行システムモデルの非決定性