Category Archives: SPINモデル検査入門

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

Posted on by 0 comment

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

第11章 ケーススタディ

  • 11.7 PROMELAによるChandy-Lamportのスナップショットアルゴリズム
    • 11.7.5 分散システムのノード
    • 11.7.6 通信チャネルの非決定的選択
      • 223ページ19行目
        numOutgoin→numOutgoing
  • 11.8 スナップショットアルゴリズムの検証

付録A ソフトウェアツール

  • A.1 SPIN
  • A.2 JSPIN
  • A.3 SPINSPIDER
    • 3行目
      必要な十分な→必要十分な?
  • A.4 VN:非決定性の視覚化

付録B リンク

「SPINモデル検査入門」は今回で終了です。お疲れ様でした。

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

Posted on by 0 comment

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

第11章 ケーススタディ

  • 11.5 分散システムのモデル化
  • 11.6 Chandy-Lamportのスナップショットアルゴリズム
    • p.213 下からl.5
      messageAtMarkerって出てこなかったけど
      → 同ページl.7のmessageAtRecoredがmessageAtmarkerの間違いなのではないか。
  • 11.7 PromelaによるChandy-Lamportのスナップショット
    • 11.7.1 モデル記述の構造
    • 11.7.2 通信チャネルリストの表現
    • 11.7.3 環境ノード
    • 11.7.4 各ノードのローカルデータ

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

Posted on by 0 comment

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

第11章 ケーススタディ

  • 11.3 リアルタイムスケジューリングアルゴリズム
    • 11.3.4 優先度を用いたスケジューラ
    • 11.3.5 RMスケジューリング
      • p.205 下の3行のデータ
        全ての(pn, en)が’,’でつないで記述され、最後だけ’.’になっている。しかし題意は、各行の(p1,e1), (p2,e2), (p3,e3)の3つの組合せのなかで、どの行の組合せが可能な優先度割り当てであるかを実験してみるとよいだろう、という事だろう。
  • 11.4 Fischerのアルゴリズム

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

Posted on by 0 comment

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

第11章 ケーススタディ

  • 11.2 非決定アルゴリズム
    • 11.2.2 有向グラフの閉路
      • 6~7行目
        2次元配列stepを実現するためにはtypedefを使う(1-6行目)とあるが、2-4行目または2-6行目では?
      • ソースコード 11.6
        19行目や20行目がfalseの場合、止まってしまうのではないか?その場合どうなる?
  • 11.3 リアルタイムスケジューリングアルゴリズム
    • 11.3.1 リアルタイムシステム
    • 11.3.2 スケジューラのPromela記述
    • 11.3.3 モデル記述の簡単化
    • 11.3.4 優先度を用いたスケジューラ(ソースコード 11.10 で使用されている通信チャネルの送信文や受信文を確認したところまで。次回は11.3.4~)
      • 4~5行目
        あるプロセス対して→あるプロセス対して?

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

Posted on by 0 comment

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

第11章 ケーススタディ

  • 11.1 通信チャネルとデータ構造
    下から3行目:
    誤:2つの疎な配列sa1とsa2を初期化し印刷する(1-19行目
    正:2つの疎な配列sa1とsa2を初期化し印刷する(1-10行目
  • 11.2 非決定アルゴリズム
    • 11.2.1 8クィーン問題

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

Posted on by 0 comment

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

第10章 通信チャネル

  • 10.3 Never claim
    • 10.3.1 安全性を表すnever claim
      • P.177 下のリスト
        ifの中、(! ((mutex)))の、mutexに二重の括弧が付いているのはどのような意味があるのだろう?
    • 10.3.2 活性を表すnever claim
    • 10.3.3 それ以外のLTL式を表すnever claim
    • 10.3.4 never claimからの参照に用いられる組込み構文
  • 10.4 非進行サイクル
    • p.184
      Spin出力のロケーションカウンタがソースコード10.3と合っていない。
      → ソースコード10.3ではプロセスPも飢餓状態になることはないと思うので、このSpinの出力はソースコード10.3のものではない?

第11章 ケーススタディ

  • 11.1 通信チャネルとデータ構造 (ソースコード6.2を思い出したところまで)

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

Posted on by 0 comment

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

第10章 Spinの高度な話題

  • 10.1 SPINの状態空間探索法
  • 10.2 検証処理の最適化
    • 10.2.1 効率の良いモデル記述
    • 10.2.2 ハッシュテーブルへのメモリ割当て
      • p.171 箇条書きの2つ目
        ハッシュテーブルに格納できる要素数→ハッシュテーブルのエントリ数?
    • 10.2.3 状態ベクタの圧縮
      • ビザンチン将軍問題
        ビザンチン将軍問題(ビザンチンしょうぐんもんだい、英語: Byzantine Generals Problem)とは、相互に通信しあう何らかのオブジェクト群において、通信および個々のオブジェクトが故障または故意によって偽の情報を伝達する可能性がある場合に、全体として正しい合意を形成できるかを問う問題である。フォールトトレラントシステムでの多数決の妥当性や分散コンピューティングの処理の妥当性に関わる問題と言える。(出典:ウィキペディア フリー百科事典
      • 検証に必要なメモリ(66Mとか23Mとか)
        実際に検証を実行した結果?
    • 10.2.4 最小オートマトン
    • 10.2.5 半順序簡約

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

Posted on by 0 comment

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

第8章 非決定性

  • 8.3 NP問題

第9章 Promelaの高度な使い方

  • 9.1 変数の属性定義
  • 9.2 組込み変数
    • 9.2.1 名前なし変数
    • 9.2.2 プロセス識別子
  • 9.3 優先度
    • 9.3.1 シミュレーション優先度
      l.15 誤植 誤「実行可能な時とき」→正「実行可能な時」
    • 9.3.2 大域的な制約を用いた優先度表現
  • 9.4 例外の表現法
  • 9.5 標準入力からの読み込み
  • 9.6 埋込みCプログラム

第10章 Spinの高度な話題

「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 ランダム受信