GLATTS勉強会ブログ

参加者 青木（読み手）、沼田、今井（記）
範囲 pp. 63 – 78

第4章 対象を広げる — Promelaの実行規則

• 4.2 Promela言語の基本
  • 4.2.1 主な構成要素
  • 4.2.2 通信チャネル
  • 4.2.3 プロセス・テンプレート定義
  • 4.2.4 その他の重要な言語要素

第5章 仕組みを理解する — SPINの検査法

• 5.1 SPINのツール概要
  • p.74 図5.1
    「ANCI Cコンパイラ」と「検証器の実行」についている†（ダガー）は、どこかで参照してる？
  • p.75 下方のコード
    なぜ、p には二つも括弧 ((p)) がついているのだろう? 自動生成時に何か都合が良い?
• 5.2 オートマトンによる形式化
  • 5.2.1 システム・オートマトンの合成

参加者 今井（読み手）、青木（記）
範囲 pp. 49 – 63

第3章 性質を表現する — 正しさの基準

• 3.2 時相論理を用いた性質表現
  • 3.2.3 進行性のLTLによる表現 (p.49の囲み記事から)
    「図3.13 CTLの時相オペレータ」の右下のグラフはおそらくAFpではなくAGpの誤り。
• 3.3 反駁のための記述
  • 3.3.1 プライオリティ逆転
  • 3.3.2 到達グラフの解析

第4章 対象を広げる

• 4.1 拡張有限状態オートマトン
  • 4.1.1 データ値の計算
  • 4.1.2 カウンタ性

参加者 青木（読み手）、沼田、今井（記）
範囲 pp. 43 – 49

第3章 性質を表現する — 正しさの基準

• 3.2 時相論理を用いた性質表現
  • 3.2.2 SPINの時相論理
    • p.43 図3.7
      図上部に「(σ, j) ⊨ p」、「命題pが状態jで成り立つ」、「σ = (s0, s1, s2, …)」、「状態の列」と、見出しのように書かれている文章は、「(σ, j) ⊨ p」の説明として、「命題pが状態jで成り立つ状態の列 σ = (s0, s1, s2, …)」という意味で書かれているのか?
  • 3.2.3 進行性のLTLによる表現 (p.49の囲み記事の前まで)

参加者 今井（読み手）、青木、沼田（記）
範囲 pp. 30 – 42

第2章 SPINをつかってみよう － Promerlaの書き方とコマンドの使い方

• 2.2 通信プロトコル
  • 2.2.3 Promela記述の詳細と解析
    • p.31～32にかけての振る舞いの確認
      Daemonプロセスをなくし、さらにReceiverプロセスを書き換えてから確認を開始しているのは、デッドロックの状況を見るため？

第3章 性質を表現する － 正しさの基準

• 3.1 プリンタとスキャナ
  • 3.1.1 デッドロック検知
    • 図3.2 l.2
      mytype→mtype
  • 3.1.2 デッドロックの解消と進行性
  • 3.1.3 タイムアウトを用いる方法
  • デッドロックの発生
• 3.2 時相論理を用いた性質表現
  • 3.2.1 検証問題

参加者 沼田（読み手）、今井（記）
範囲 pp. 15 – 30

第2章 SPINをつかってみよう — Promerlaの書き方とコマンドの使い方

• 2.1 簡単な並行実行プロセス
  • 2.1.1 Promelaプロセスの基本
  • 2.1.2 プロセス数の増加
  • 2.1.3 不具合の自動検知法 — assert文
  • 2.1.4 読み易さの向上
• 2.2 通信プロトコル
  • 2.2.1 ABPの問題
  • 2.2.2 Promelaによるモデル化

参加者 今井（読み手）、青木（記）
範囲 pp. 6 – 14

第1章 モデル検査とは — 自動検査とモデル検査法

• 1.2 モデル検査法の発展
  • 1.2.1 CTL記号モデル検査法
    ・「∈」は集合に含まれること、「|=」の意味はわかりませんでした。
    ・SMVはSymbolic Model Verifierの略。
  • 1.2.2 有界モデル検査法
  • 1.2.3 オートマトンに基づくモデル検査法
    ・「⊆」は部分集合を表す。
    ・「冪オーダー」は「べきおーだー」と読む。冪はべき乗のべき。
  • モデルのいろいろ

「SPINモデル検査」1.1.2の図1.3を合成してみました。Q側遷移から深さ優先で探索しました。(今井)

参加者 青木（読み手）、沼田、今井（記）
範囲 pp. i – 6

序文

まえがき

• SPINとは
• SPINとの出会い
• 本書の特徴
  • p. v 本節下から2行目
    パソコンにインスールして → パソコンにインストールして
• 本書の構成と読み方のガイド
  • p. v 第2章 見出しの最後
    使い方門 → 使い方
  • p. v 下から2行目
    「反駁」の読み方は? → はんばく
• SPINの入手法
• 謝辞

目次

（まえがきに「本書の構成と読み方のガイド」があったので、読むのを省略）

第1章 モデル検査とは — 自動検査とモデル検査法

• 1.1 振舞い仕様とモデル検査法
  • 1.1.1 振舞い仕様と状態遷移システム
  • 1.1.2 状態空間の網羅的な探索
    • p. 5 図1.3
      copyやpr.putなど、状態を表す○の真上に書かれているものがあるが、状態名を表しているのではなく、pr.getなどと同様、遷移のイベント。
    • p. 6 図1.4
      図1.3を合成して図1.4になることを確かめておこう。