Monthly Archives: 5月 2011

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

Posted on by 0 comment

参加者 青木(読み手)、沼田、今井(記)
範囲 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 システム・オートマトンの合成

「SPINモデル検査」第6回(5月27日)

Posted on by 0 comment

参加者 今井(読み手)、青木(記)
範囲 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 カウンタ性

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

Posted on by 0 comment

参加者 青木(読み手)、沼田、今井(記)
範囲 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の囲み記事の前まで)

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

Posted on by 0 comment

参加者 今井(読み手)、青木、沼田(記)
範囲 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 検証問題

「SPINモデル検査」第3回(5月17日)

Posted on by 0 comment

参加者 沼田(読み手)、今井(記)
範囲 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によるモデル化

    「SPINモデル検査」第2回(5月13日)

    Posted on by 0 comment

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

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

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

    「SPINモデル検査」図1.3 → 図1.4

    Posted on by 0 comment

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

    「SPINモデル検査」第1回(5月10日)

    Posted on by 1 comment

    参加者 青木(読み手)、沼田、今井(記)
    範囲 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になることを確かめておこう。

    次の書籍

    Posted on by 4 comments

    沼田です。

    SPINモデル検査入門を前回で読み終わりました。

    次の本として読みたいものをこの記事のコメントにあげたいと思います。

    よろしくお願いします。

    Category: information