SPIN を使ったモデル検査の入門 #Spin

今年は PlantUML を使って多くの仕様を図にして書き直しました。文字の仕様を図にする
ことでより理解が深まるものです。ただし文字が図になったからといって勘違いや検討漏れなど、同じような課題が残ります。
こういうときに便利なのが形式仕様記述ではないでしょうか。
そんなわけでモデル検査法に基づく自動検証ツール SPIN について、この本で覚え立てほやほやですがまとめてみました。

SPIN モデル検査近代科学社

まずどう使うのかをクライアントが 1 台、サーバが 1 台のシステムを通して紹介します。

このシステムはクライアントがサーバにリクエストすると、サーバはクライアントにレスポンスを返します。クライアントはそのレスポンスを特に使いません。通信は片方向のみです。
このシステムがとる状態に適当な名前を付けて状態遷移図を書いてみます。

この状態遷移がシステムの満たすべき仕様です。これを SPIN でデバッグできるようにします。SPIN では仕様を仕様言語 Promela で記述します。

Promela Manual Pages -- Index

mtype = { Start, Processing, End };
mtype turn = Start;

active proctype Client()
{
  do
    :: (turn == Start) -> printf("ping"); turn = Processing;
  od
}

active proctype Server()
{
  do
    :: (turn == Processing) -> printf("pong"); turn = End;
  od
}

このソースコードはアプリケーションの状態を表すグローバル変数があって、クライアントとサーバが値の変化を見て動きます。
これを spin コマンドで検証できます。-u は実行するステップ数くらいで見てください。

Spin Run-Time Options

$ spin -u10 uni.pml
      ping          pong      timeout
#processes: 2
                turn = End
  8:    proc  1 (Server:1) uni.pml:13 (state 4)
  8:    proc  0 (Client:1) uni.pml:6 (state 4)
2 processes created
$

クライアントからの ping とサーバからの pong が出力されました。これが SPIN を使った設計のデバッグです。
ではもう少し具体的なアプリケーションとしてクライアントが 1 台、サーバが 2 台の双方向通信について考えてみます。

次にシステムがとる状態を考えてみましょう、といってもまだ形もなにもないシステムがとる状態を考えるのは難しいものです。
当てずっぽうで状態遷移図を作ってみます。

ずいぶん曖昧なものができてきました。
このシステムもクライアントがサーバにリクエストして、サーバはクライアントにレスポンスを返すものとします。
ここで Promela を書いてもいいんですが socat を使って通信の雰囲気を見てみます。

# echo client
echo | socat - UDP4-DATAGRAM:255.255.255.255:19541,broadcast

# echo server
socat udp-listen:19541,fork SYSTEM:'echo $$'

実行してみます。サーバのプロセスは先に 2 個起動しておいて、クライアントからリクエストするとサーバがレスポンスを返してきました。通信内容は特に意味はありません。

$ echo | socat - UDP4-DATAGRAM:255.255.255.255:19541,broadcast
85689
85690
$

これなら通信の仕組み自体を動かして確認できます。仕様としては socat の実装に依存していて表現力は弱いですが、それっぽく動けてそうですね。
ではこの仕様を Promela で書き直してみます。

#define SERVER_COUNT 2
mtype = { Start, Request, Processing, Response, End };
mtype turn = Start;
chan response = [SERVER_COUNT] of {mtype, pid}

active proctype Client()
{
  pid x;

  do
    :: (turn == Start) -> turn = Request;
    :: (len(response) == SERVER_COUNT) -> turn = Response;
    :: (turn == Response) -> atomic {
        if
          :: (len(response) == 0) -> turn = End;
          :: response ? Response(x) -> printf("Client Recieved. pid:%d\n", x);
        fi;
    }
  od;
}

active [SERVER_COUNT] proctype Server()
{
  do
    :: (turn == Request) && !(response ? [Response(_pid)]) -> atomic {
      response ! Response(_pid);
    }
  od;
}

この仕様を動かします。

$ spin -c10 bi.pml
proc 0 = Client
proc 1 = Server
proc 2 = Server
q\p   0   1   2
  1   .   .   response!Response,2
  1   .   response!Response,1
  1   response?Response,2
      Client Recieved. pid:2
  1   response?Response,1
      Client Recieved. pid:1
      timeout
-------------
final state:
-------------
#processes: 3
                turn = End
                queue 1 (response):
                servers = 2
 27:    proc  2 (Server:1) bi.pml:25 (state 4)
 27:    proc  1 (Server:1) bi.pml:25 (state 4)
 27:    proc  0 (Client:1) bi.pml:11 (state 13)
3 processes created
$

プロセス ID の 0 がクライアント、1 と 2 がサーバです。socat と同じようにそれぞれが動いてますね。
ではさらにシミュレーションを繰り返してみます。

$ spin -c10 bi.pml
proc 0 = Client
proc 1 = Server
proc 2 = Server
q\p   0   1   2
  1   .   .   response!Response,2
      timeout
-------------
final state:
-------------
#processes: 3
                turn = Request
                queue 1 (response): [Response,2]
                servers = 2
  6:    proc  2 (Server:1) bi.pml:25 (state 4)
  6:    proc  1 (Server:1) bi.pml:25 (state 4)
  6:    proc  0 (Client:1) bi.pml:11 (state 13)
3 processes created
$

今度はクライアントが何も出力していません。socat を使ったときはこのようなことはありませんでした。所々 timeout と書いてる通り、実際のシステムは通信が失敗したりノードが応答不能になってることが考えられます。こんな風にして元々の状態遷移図にはなかった状態を見つけて、仕様の検討漏れを洗い出すことができます。

まだ SPIN も Promela も使い方に自信はないんですが、仕様のデバッグについて自分事として考えてようやく入門できた気分です。
来年中にはもうちょっと自信をもって使えるようにがんばります。