Skip to content

Instantly share code, notes, and snippets.

@y-taka-23

y-taka-23/seminar_20140130.md

Created January 14, 2014 14:29
Show Gist options
  • Star 2 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save y-taka-23/8419128 to your computer and use it in GitHub Desktop.
Save y-taka-23/8419128 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
seminar_20140130.md

名古屋モデル検査勉強会 #2

前回の勉強会では Promela の文法要素と基本的な SPIN の使い方を眺めたので、今回は LTL 式を用いた性質検査およびハンズオンを行う。

LTL 式による検査

LTL 式の構文

SPIN の LTL は命題論理の拡張となっており、各論理式の真偽が状態に依存する。

論理演算子 ! && || -> および <-> は通常の意味で使用可能である。

その他に、時相論理演算子として主に [] <> Uが使用できる。状態 s0 において、それぞれの意味は以下の通り。ここで不等号は状態遷移による時間的な前後関係を表す。

  • [] p : s0 <= s を満たす任意の状態 s において p が真
  • <> p : s0 <= s を満たすある状態 s が存在し、s において p が真
  • p U q : s0 <= s を満たすある状態 s が存在し、s0 <= s' < s を満たす任意の状態 s' において p が真、かつ s において q が真

さらに使いこなしたい人は LTL 式の頻出パターンも参照のこと。

SPIN による検査

  1. ファイル (拡張子は通例 prp) に検査したい LTL 式の__否定__を記述
  2. オプション -F の引数にそのファイルを指定して SPIN を実行
  3. 通常通り gcc でコンパイル
  4. 生成された検証器にオプション -a を指定して実行
  5. __否定する前__のLTL 式が成り立たない場合、assertion violated または acceptance cycle として検出される
spin -a -F formula.prp model.pml
gcc -o pan pan.c
./pan -a

リモート参照

LTL 式を記述する際には、<procname>@<labelname> でプロセスのロケーションカウンタが指定したラベル位置にあるかどうかを bool 型で取得できる。また <procname>:<varname> でプロセスローカル変数の値を取得できる。

ただし、これらの式を直接 prp ファイル中に記述してもエラーとなるため、pml ファイルの中で #define を用いて変数名を付けておく必要がある。ちなみにその際、変数名には何故か小文字しか使用できない。

never claim

SPIN は与えられた LTL 式を never claim と呼ばれるプロセスに変換した後、元のモデルと never claim との積オートマトンを検査する。

never claim 自体をファイルに書き出して確認したい場合は、SPIN に対して pml ファイルなしで -F オプションを与えればよい。拡張子には通例 ltl が用いられる。読み込む際には -N オプションを指定すればよい。

spin -F formula.prp > formula.ltl
spin -a -N formula.ltl formula.pml

練習問題 : Android の push 通知

Android 端末における、アプリケーションからの push 通知をモデル化することを考える。push 通知はアプリケーションサーバから端末に対して直接送るわけではなく、次のように GCM (Google Cloud Messaging) サーバを経由する。

  1. 各端末は device token と呼ばれる識別子で区別される。
  2. アプリケーションサーバは push 通知を送りたい端末の device token と送りたい内容を、GCM サーバに依頼する。
  3. GCM サーバは依頼された device token に紐付いている端末に対して push 通知を送信する。

さらに、GCM サーバは不定期に device token を変更する。ただし、変更後にはある程度の移行期間が設けられている。移行期間中は古い device token でも依頼を行うことができ、この際 GCM サーバからアプリケーションサーバに新しい device token が通知される。移行期間終了後に古い device token で依頼を行うとエラーになる。

条件

  1. 今回は問題を単純化するため以下の仮定を置く。
    • push 通知の内容は常に同じであるとしてよい。
    • 端末側の設定は、常に push 通信許可になっているとしてよい。
    • 初期状態ではアプリはインストール済み、device token は同期済みとする。また途中でアプリがアンインストールされることもないとする。
    • 複数端末への同時 push 通知は考えなくてよい。
  2. アプリケーションサーバと GCM サーバ間の通信は即座に行われる。端末と GCM サーバ間の通信は、電波状況により遅延が発生する可能性がある。いずれの通信路でも、内容の誤りや消失は発生しないとしてよい。
  3. 端末とアプリケーションサーバ間で直接通信する機会はないとする。

問題

  1. 上記の設定をモデル化し、どのような条件でエラーとなるか確認せよ。
  2. GCM サーバに「device token 変更後、push 依頼を受信するまでは勝手に移行期間を終わらせない」機能を実装し、このときエラーが生じなくなることを確認せよ。
  3. 上記 2 の機能の仕様「移行期間の終了は push 依頼送信後にしか発生しないこと」を検査せよ。
  4. 上記 2 の機能により「アプリケーションサーバが push 依頼を送信すると、必ず push 通知が端末に到達すること」を検査せよ。
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment