Top / システム検証例
エレベーターモデルの検証 †
pn(1).//乗客の数
fn(2).//フロアの数
//フロアの生成
fn(F) :- F0=F-1,F>0 | fn(F0),
{ f(F0),btn(false).
//乗客の出入り
p,elv{open(1),$p} :- elv{p,open(1),$p}.
elv{p,open(1),$p} :- p,elv{open(1),$p}.
}.
//乗客の生成
pn(P),{ f(F),$p,@p } :- P0=P-1,P>0,int(F) | pn(P0),{ p,f(F),$p,@p }.
//エレベーターの生成
pn(0),fn(0),{ f(F),$p,@p } :- int(F) | { elv{open(1),act(null),to(0)},f(F),$p,@p }.
//乗客の動作
//フロアにいる乗客がボタンを押す
{ p,btn(false),$p,@p } :- { p,btn(true),$p,@p }.
//エレベーター中にいる乗客がボタンを押す
{ elv{p,to(0),$q[]},$p1[],@p1 },{ f(F),$p2[],@p2 }
:- int(F) | { elv{p,to(F),$q[]},$p1[],@p1 },{ f(F),$p2[],@p2 }.
//エレベーターの動作
//エレベーターのドアを閉める
{ elv{open(Op),act(close),$q},$p,@p } :- int(Op) | { elv{open(0),act(null),$q},$p,@p }.
//エレベーターのドアをあける
{ elv{open(Op),act(open),$q},$p,@p } :- int(Op) | { elv{open(1),act(null),$q},$p,@p }.
//エレベーターの移動
{ elv{act(move(M)),$q[] },$p1[],@p1 },{ f(F),$p2[],@p2 }
:- M=:=F | { $p1[],@p1 },{ elv{act(null),$q[]},f(F),$p2[],@p2 }.
//エレベーターの不移動
{ f(F),elv{act(move(M)),$q[] },$p[],@p }
:- F=:=M | { f(F),elv{act(null),$q[]},$p[],@p }.
//コントローラー
cnt(null).
//ドアを閉じる命令を送信(エレベーター内から受信)
cnt(null),{ elv{act(null),to(T),$q[]},$p[],@p }
:- int(T) | cnt(move(T)),{ elv{act(close),to(T),$q[]},$p[],@p }.
//ドアを閉じる命令を送信(フロアのボタンから受信)
cnt(null),{ f(F),btn(true),$p1[],@p1 },{ elv{act(null),$q[]},$p2[],@p2 }
:- int(F) | cnt(move(F)),{ f(F),btn(true),$p1[],@p1 },{ elv{act(close),$q[]},$p2[],@p2 }.
//移動命令を送信
cnt(move(F)),{ elv{act(null),$q[]},$p[],@p }
:- int(F) | cnt(end),{ elv{act(move(F)),$q[]},$p[],@p }.
//ドアを開く命令を送信
cnt(end),{ btn(B),elv{act(null),to(T),$q[]},$p[],@p }
:- unary(B),int(T) | cnt(null),{ btn(false),elv{act(open),to(0),$q[]},$p[],@p }.
検証項目 †
「エレベーターはドアを開けたまま動くことはない」
シンボル定義：p = { elv{open(1),act(move(M)),$q},$p,@p } :- int(M)
仕様：!<>p
モデル検査をすると、このモデルではそのようなことがないことが分かる。
Sliding Window Protocolの検証 †
{
wSize(2). // ウィンドウサイズ
nMAX(3). // 再送処理などの制御に利用するナンバーnの上限値
idMAX(3). // 送信データの正当さをチェックするidの上限値
error(false). // エラー検出フラグ
sender{ n(0), nextId(0), sucId(0), c(0) }. // データ送信者
ss=rr. // データが通る通信路
rs=sr. // ACKが通る通信路
receiver{ n(0), expId(0) }. // データ受信者
// 送信者 : データの送信 sender -> [data]
sd@@ sender{ n(N), nextId(ID), sucId(SucID), c(C) }, nMAX(NMAX), idMAX(IDMAX), wSize(W), ss=SC
:- C<W, C_=C+1, DN=(N+C) mod NMAX, ID_=(ID+1) mod IDMAX, int(SucID)
| sender{ n(N), nextId(ID_),sucId(SucID), c(C_)}, nMAX(NMAX), idMAX(IDMAX), wSize(W), ss=[data(DN,ID)|SC].
// 受信者 : データ受信，ACKの返送(予期していたデータ) [data] -> receiver -> [ack]
rs@@ receiver{ n(N), expId(EID) }, nMAX(NMAX), idMAX(IDMAX), SC=[data(DN,ID)|rr], rs=RC
:- N=:=DN, EID=:=ID, N_=(N+1) mod NMAX, EID_=(EID+1) mod IDMAX
| receiver{ n(N_),expId(EID_)}, nMAX(NMAX), idMAX(IDMAX), SC=rr, rs=[ack(DN)|RC].
// 受信者 : データ受信，データ破棄(受信するはずのデータの消失検出) [data] -> []
ru@@ receiver{ n(N), expId(EID) }, SC=[data(DN,ID)|rr]
:- N=\=DN, int(ID), int(EID), ground(SC)
| receiver{ n(N), expId(EID) }, SC=rr.
// 受信者 : データ受信(正しいメッセージでない) [data] -> receiver -> error
re@@ error(false), receiver{ n(N), expId(EID) }, SC=[data(DN,ID)|rr], rs=RC, sender{ $p[] }
:- N=:=DN, EID=\=ID, ground(SC), ground(RC)
| error(true).
// 送信者 : ACKの受信(予期していたACK) [ack] -> slide
s@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, nMAX(NMAX), idMAX(IDMAX), RC=[ack(ACK)|sr]
:- N=:=ACK, C>0, N_=(N+1) mod NMAX, SucID_=(SucID+1) mod IDMAX, C_=C-1, int(NextID)
| sender{ n(N_),nextId(NextID), sucId(SucID_),c(C_)}, nMAX(NMAX), idMAX(IDMAX), RC=sr.
// 送信者 : ACKの受信，ACKの破棄(データかACKの消失検出) [ack] -> []
r@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, RC=[ack(ACK)|sr]
:- N=\=ACK, int(NextID), int(SucID), int(C)
| sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, RC=sr.
// 送信者 : タイムアウトの検出 [timeout] -> reset
t@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, timeout
:- int(N), int(NextID), int(SucID), int(C)
| sender{ n(N), nextId(SucID), sucId(SucID), c(0) }.
// 通信路 : データ,ACKの消失 [data] -> [], [ack] -> []
ld@@ X=[data(DN,ID)|Y] :- int(DN),int(ID) | X=Y.
la@@ X=[ack(ACK)|Y] :- int(ACK) | X=Y .
}.
// タイムアウトの発生 [] -> [timeout]
o@@ { error(false), $p, @p }/ :- { timeout, error(false), $p, @p }.
検証項目 †
「データを送信すれば必ず返信が返ってくる」
シンボル定義：
send = { C=data(DN,ID),$p,@p } :- int(DN), int(ID), ground(C) |
ack = { C=ack(ACK),$p,@p } :- int(ACK), ground(C) |
仕様：[](send -> <>ack)
モデル検査をすると「データを送信すると、通信路でデータ消滅してしまうことが繰り返し続く」という経路が見つかる。
つまり、このモデルでは通信路が途切れている場合、この仕様は満たされないことを示している。
水差しで量れる水量の検証 †
% pot(現在の容量,最大容量) pot(0,300). pot(0,700). % 空にする pot(X,MAX) :- X>0 | pot(0,MAX). % 満杯にする pot(X,MAX) :- X<MAX | pot(MAX,MAX). % 自分が空になるまで移す pot(X,MX), pot(Y,MY) :- X>0, Y<MY, Z=X+Y, Z=<MY | pot(0, MX), pot(Z, MY). % 相手が満杯になるまで移す pot(X,MX), pot(Y,MY) :- X>0, Y<MY, Z=X-(MY-Y), Z>=0 | pot(Z,MX), pot(MY,MY).
検証項目 †
「300mlと700mlの水差しから500mlの水が量れる」
StateViewer?の状態検索機能を使うと量れることがわかる。
経路を順に見ていくと以下の操作をすることで500mlを量れる
pot(現在の容量,最大容量) 1. pot(0,300). pot(0,700). 2. pot(0,300). pot(700,700). 3. pot(300,300). pot(400,700). 4. pot(0,300). pot(400,700). 5. pot(300,300). pot(100,700). 6. pot(0,300). pot(100,700). 7. pot(100,300). pot(0,700). 8. pot(100,300). pot(700,700). 9. pot(300,300). pot(500,700).
Attached files
- Attach file:
swp.jpg 595 download
[Information]
elv.jpg 647 download
[Information]
pot.jpg 622 download
[Information]
