Monthly Archives: 6月 2011

「SPINモデル検査」第15回(6月28日)

Posted on by 0 comment

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

第7章 ケーススタディ(2) モデル検査を使い分ける — Java並行プログラムの解析

  • 7.3 入れ子モニターの不具合
    • 7.3.3 抽象レベルのデザイン解析

第8章 ケーススタディ(3) 組込みソフトウェアの解析に使う —システムソフトウェアへの適用
※捨象(シャショウ)とは、事物または表象からある要素・側面・性質を抽象するとき、他の要素・側面・性質を度外視すること(コトバンクより)。

  • 8.1 割り込み処理と共有資源
    • 8.1.1 割り込み処理の表現
    • 8.1.2 記述と解析の例

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

Posted on by 0 comment

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

第7章 ケーススタディ(2) モデル検査を使い分ける — Java並行プログラムの解析

  • 7.2 Javaの並行同期機構
    • 7.2.1 Javaが提供するAPI
      p.135 l.2 誤植 誤:synchronzied 正:synchronized
    • 7.2.2 Promelaによる表現
  • 7.3 入れ子モニターの不具合
    • 7.3.1 セマフォの利用
      p.139 l.10 誤植 downを通過を
      p.140 図7.8等誤植 誤:InterruptException 正:InterruptedException
    • 7.3.2 Promela同期ライブラリの利用

「SPINモデル検査」第13回(6月21日)

Posted on by 0 comment

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

第6章 ケーススタディ(1) ソフトウェアデザインを検証する — 状態遷移ダイアグラムの解析

  • 6.3 バリエーション
    • 6.3.1 ブロードキャスト・イベント (p.122 図6.31 ~)
    • 6.3.2 階層型状態遷移ダイアグラム

第7章 ケーススタディ(2) モデル検査を使い分ける — Java並行プログラムの解析

  • 7.1 デザイン検証とJavaプログラム
    • 7.1.1 有限バッファのPromela記述
    • 7.1.2 有限バッファのJava記述

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

Posted on by 0 comment

参加者 今井(読み手)、沼田、青木(記)

範囲 pp. 111 – p.122

第6章 ケーススタディ(1) ソフトウェアデザインを検証する — 状態遷移ダイアグラムの解析

  • 6.2 分散協調システム
    • 6.2.1 遠隔操作ロボット
      誤植? 図6.19のソースコード6行目StartButtonの後の「:」は「;」の誤りでしょうか?
  • 6.3 バリエーション
    • 6.3.1 ブロードキャスト・イベント(図6.31の上まで)
      誤植:図6.28と図6.29のソースコード 正「active proctype」、誤「acrive proctype」

「SPINモデル検査」第11回(6月14日)

Posted on by 0 comment

参加者 沼田(読み手)、今井、青木(記)

範囲 pp. 99 – p.110

第6章 ケーススタディ(1) ソフトウェアデザインを検証する — 状態遷移ダイアグラムの解析

  • 6.1 状態遷移システム
    • 6.1.1 状態遷移マシン (p.99 中ほど、図6.2の遷移ラベルの説明の後から)
      誤植:p.103 ソースコードの5行目のdoブロックの終わりがodの誤り。
      同ソースコードの8行目のatomicブロックの閉じ括弧がない。
    • 6.1.2 簡単な航行制御システム
      誤植:p.106 図6.11のActive状態の囲みのreseumeはresumeの誤り。
      「ゴリラ利用者」、「ゴリラ・シナリオ」は初めての言葉だったので、インターネットで検索してみましたがヒットしませんでした。乱暴な感じを表現しているのかなと思いました。

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

Posted on by 0 comment

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

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

  • 5.4 時相論理との関係
    • 5.4.2 Büchiオートマトンの生成 (p.92 中ほど、図5.19の説明から)

第6章 ケーススタディ(1) ソフトウェアデザインを検証する — 状態遷移ダイアグラムの解析

  • 6.1 状態遷移システム
    • 6.1.1 状態遷移マシン (p.99 中ほど、図6.2の遷移ラベルの説明まで)

「SPINモデル検査」第9回(6月7日)

Posted on by 0 comment

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

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

  • 5.3 状態空間の探索法
    • 5.3.2 進行性解析とLTLモデル検査
    • SPINの工夫
  • 5.4 時相論理との関係
    • 5.4.1 準備
      • LTLオペレータのVはどんな意味?
    • 5.4.2 Büchiオートマトンの生成
      • 次回は図5.19~

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

Posted on by 0 comment

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

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

  • 5.2 オートマトンによる形式化
    • 5.2.2 性質オートマトンの追加
  • 5.3 状態空間の探索法
    • 5.3.1 到達性の解析