前回の勉強会では Promela の文法要素と基本的な SPIN の使い方を眺めたので、今回は 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 式の頻出パターンも参照のこと。
- ファイル (拡張子は通例 prp) に検査したい LTL 式の__否定__を記述
- オプション
-F
の引数にそのファイルを指定して SPIN を実行 - 通常通り gcc でコンパイル
- 生成された検証器にオプション
-a
を指定して実行 - __否定する前__の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
を用いて変数名を付けておく必要がある。ちなみにその際、変数名には何故か小文字しか使用できない。
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 通知をモデル化することを考える。push 通知はアプリケーションサーバから端末に対して直接送るわけではなく、次のように GCM (Google Cloud Messaging) サーバを経由する。
- 各端末は device token と呼ばれる識別子で区別される。
- アプリケーションサーバは push 通知を送りたい端末の device token と送りたい内容を、GCM サーバに依頼する。
- GCM サーバは依頼された device token に紐付いている端末に対して push 通知を送信する。
さらに、GCM サーバは不定期に device token を変更する。ただし、変更後にはある程度の移行期間が設けられている。移行期間中は古い device token でも依頼を行うことができ、この際 GCM サーバからアプリケーションサーバに新しい device token が通知される。移行期間終了後に古い device token で依頼を行うとエラーになる。
- 今回は問題を単純化するため以下の仮定を置く。
- push 通知の内容は常に同じであるとしてよい。
- 端末側の設定は、常に push 通信許可になっているとしてよい。
- 初期状態ではアプリはインストール済み、device token は同期済みとする。また途中でアプリがアンインストールされることもないとする。
- 複数端末への同時 push 通知は考えなくてよい。
- アプリケーションサーバと GCM サーバ間の通信は即座に行われる。端末と GCM サーバ間の通信は、電波状況により遅延が発生する可能性がある。いずれの通信路でも、内容の誤りや消失は発生しないとしてよい。
- 端末とアプリケーションサーバ間で直接通信する機会はないとする。
- 上記の設定をモデル化し、どのような条件でエラーとなるか確認せよ。
- GCM サーバに「device token 変更後、push 依頼を受信するまでは勝手に移行期間を終わらせない」機能を実装し、このときエラーが生じなくなることを確認せよ。
- 上記 2 の機能の仕様「移行期間の終了は push 依頼送信後にしか発生しないこと」を検査せよ。
- 上記 2 の機能により「アプリケーションサーバが push 依頼を送信すると、必ず push 通知が端末に到達すること」を検査せよ。