① SEQ ド Q[1 ]

②

Yi

(i

E

I) 

[SEQ  1 =   B [ i ] コ C [ i ]] 

ただし，

1 

は正整数の集合を表す。

上述の①，②が成立すれば，仮定

B[l

，]

B[2

]，…をすべて満たす状態 列

σ

に対しては，

n e x t ̲ r e q u i r e d

の値が無限に大きくなるといえる。

以下では，

(A) 

SDT

プロトコルの進行性の検証において局や回線に対して具体的にど のような仮定を置いたか，

(日検証に必要な補題をどのように定めたか，

(C)  (A)，  (B)の仮定や補題から①，②をどのように証明したか，

について順に述べる。

6.4.2 

局や回線に対する仮定

[  1 ]   TRANSMES

， 

FINDTO

， 

RETRAN

のように，システムが能動的に 行う状態遷移関数については，

6.3.2.2

の

( 1 )

の

α

に

TRANSMES

，

FIN‑

DTO[

i]， 

RETRAN[

i]を代入した式

(1 ‑1) 

口(口く

)okTRANSMES

コく

) l a s tTRANSMES} 

(1 ‑2)  YiEI 

[口{口く

)okFINDTO 

[i]コく

) l a s tFINDTO 

[i] } ] 

第6章 代数的に記述された通信プロトコルの動的性質の検証 99 

(1 ‑3)  ViεI 

[口(口く

)okRETRAN 

[i]コく

) l a s tRETRAN 

[i] } ]  を仮定する(以下 (1‑1)‑(1‑2) の三つの仮定を

B l 'ViEI {B

2 [i]}， 

V  iEI { B 3  

[i]}で表す〉。

[  2  ] 

受信を表す状態遷移関数

RECM&  TRANA

については，

6.3.2. 

2の(2)のα，βにそれぞれ

RETRAN[

i]，

RECM 

& 

TRANA

 i，[ j]を代入 した式

(2 ‑ 1) 

Vi

， 

jEI 

[口{(口く

) l a s tRETRAN 

[i] 

AND

口く

)okRECM 

& 

TRAN  A  [ i

， j]) 

コく

) l a s tRECM 

& 

TRANA[i

， j]}] 

を仮定とする。また，状態遷移関数

RECEIVEA

[i]についても同様に，式

(  2  ‑2  ) Vi

， j E 

I 

[口{(口く)

l a s tRECM  &  TRANA[

i] 

AND 

口く

)okRECEIVEA 

[j] ) 

コく>

l a s t   RECEIVEA 

[j] } ] 

を仮定する(以下，仮定(2 ‑ 1)， (2 ‑ 2 )をそれぞれ

Vi

，

jEI 

{B₄

[ i

， j]}， 

Vi

， 

jEI { B 5  

 ，[i j]}で表す〉。

実際に，各 iに対して

SEQ ト B[

i]コ

C[

i]"を証明する場合，受信局が シーケンス番号 iのノξケットを受信したときに返送する確認パケットのシーケ ンス番号

j

が 豆

j

豆

i+TWS

のようにウインドサイズ

(TWS)

の範囲でしか 変化しないため，仮定(2 ‑ 1)， (2 ‑ 2 )については

j

の値に

i

から

i+TWS

までの整数値を代入した

( j

を含まなしう

TWS+1

個の式を仮定として用い る。仮定(2 ‑ 1)， (2 ‑ 2 )の

B 4 [ i

， 

j ]

， 

B 5   [ i

， 

j ]

の引数

j

_{~こ代入できるの} は，定義より正整数のみであるが，

B

4

[ i

， 

j+k]

， Ci

kE

I)のような正整数の和 についても代入を許すことにする。ただし，

1  +  1

が

2

であるといったテンポ

ラルロジックの外で与えられている性質は用いない(このため， B[ 1， 1 

+ 

1 ]  と

B[

 ，1

2]

は異なるテンポラルロジックの式を表す〉。以下，

B l '   B

2 [i] ， 

B 3   [ i

 ，]

B 4   [ i

， i]， 

B4  [ i

， 

i  + 1 

]，…， 

B4 

[i， 

i  +  TWS

 ，]

B 5  

[i， 

i ]

， 

B 5  

 [i，

i  + 

1 

]，…， 

B 5  

， i[

i  +TWS]

のような

2xTWS+ 5

個の仮定の論理積を

B[

i]で表

100  第6章 代数的に記述された通信プロトコルの動的性質の検証 し，

B[

i]を局や回線に対する仮定とする。

6.4.3 

動的性質の検証に用いる静的な性質

6.4.1

の②が成り立つためには，

l o w e s t  unacked

の値を大きくしていか なければならない。

そして，シーケンス番号が

l o w e s tunacked

の値(以下

i

で表す〉に等しい パケットがどのような状況にあるかを分類すると，

(1)  シーケンス番号 iのノミケットがまだ送信されていない

(2')  少なくとも一度は送信したけれど，相手局が未だそのノミケットを受信し ていない

(4')  相手局が受信し，確認パケットが返送されたが，送信局が未だ受信して いない

という三つの状況が考えられる。さらに，各状況をもう少し詳細に分類すると，

(3)  回線等のエラーで， (2')の状況でタイムアウトが発生し，再送の準備を 行っている。

(5)  同様に， (4')の状況でタイムアウトが発生した

とし、う特殊な状況も考えられる(なお， (2')， (4')の状況で (3)，(5)に該当しない 状況をそれぞれ (2)，(4)で表す〉。

ここで，次のような五つの述語

Q1‑Q5

を用いると， (1)から

( 5 )

の各状況 に属する状態

t

が，

Qk(t

， i) 

E  TRUE (  1

豆

k

豆

5)

を満たすように定義でき る。

(1) 

Q 

1 (t， i) 

会

V a l i d ( t )AND l o w e s t  u n a c k e d ( t )  =i  AND  h i g h e s t  s e n t ( t )   +  1

壬

i

(2)  Q 2 (t， i) 

全

V a l i d ( t )AND  l o w e s t  u n a c k e d ( t )

ニ

i AND  h i g h e s t  s e n t ( t )   +  1  >i 

AND  t i m e r ̲ r u n n i n g ( t

， i) 

AND  NOT(already r e c e i v e d ( t

， i)) 

第6章 代 数 的 に 記 述 さ れ た 通 信 プ ロ ト コ ル の 動 的 性 質 の 検 証 101  (3) 

Q 

3 (t， i) 

全

V a l i d ( t )AND  l o w e s t  u n a c k e d ( t )  

= 

i  AND  h i g h e s t  s e n t ( t ) +  1  >i 

AND  NOT(timer r u n n i n g ( t

， i)) 

AND  NOT(already r e c e i v e d ( t

， i))  (4)  Q 4 (t， i) 

全

V a l i d ( t )AND  l o w e s t  u n a c k e d ( t )   =  i  AND  h i g h e s t  s e n t ( t )  + 1  >  i 

AND  t i m e r  r u n n i n g ( t

， i) 

AND  a l r e a d y   ̲ r e c e i v e d ( t

， i)  (5)  Q 5 (t， i) 

全

V a l i d ( t )AND  l o w e s t  u n a c k e d ( t )

二

i AND  h i g h e s t  s e n t ( t )  + 1  >  i 

AND NOT(timer r u n n i n g ( t

， 

i ) )   AND  a l r e a d y  r e c e i v e d ( t

， i) 

このとき， Q[i] 

( t )   E 

Q 

1  ( t

， i) 

OR 

Q 

2  ( t

， i)

OR … OR 

Q 

5  ( t

， i)が成立 する[5へまた， Q 

6  ( t

， i)を

l o w e s tu n a c k e d ( t )

の値が

i

より大きいこと，

すなわち，

(6)  Q 6 (t， i)会 Q'[i] (t)  とすると，

6.4. 1

で、述べた式

C [

^i]会口 {Q[i]つく)Q'[i]}  が真であることと，式

口{Q

1  [ i ]   OR  … OR 

Q 

5  [ i ]コ

<)Q

6 

[i]} 

が真であることとが等価になる。従って， (1)‑(5)に属する状態が有限回の状態 遷移で(6)に属する状態に遷移することが証明できれば

C [

i]が真になる。

そこで，(1

) ‑ ( 6 )

に属する各状態が

SDT

プロトコルで、許される

1

回の動作(状 態遷移関数〉でどの状況に属する状態に遷移するかをチェックし，それらの関 係を6. 3 . 2 . 3で述べた方法に従って，テンポラルロジックの式に変換する。

例えば， (1)については， Q 1 (t， i)

τTRUE

を満たす任意の状態tに対して，

102  第6章 代数的に記述された通信プロトコルの動的性質の検証

送信動作

TRANSMES

が実行可能であり，送信動作を実行すれば， (2)に属す る状態に遷移する。また，送信動作以外の実行可能な動作に対しては，動作実 行後も(1)にとどまる。これらの性質を代数的な定理の形で表すと，

く

1> ¥ l tES  ¥ l iεI 

[Q 

1 

( t

， i)コ

Valid(TRANSMES(t))] E  TRUE 

く

2 > ¥ l tES  ¥ l iEI 

[Q  1  ( t

， i)コ

Q 2  (TRANSMES(t)

， i)] 

E  TRUE 

く

3 > ¥ 1 α

宇

TRANSMES ¥ l tES  ¥ l iεI 

[Q 

1 

( t

， i) 

AND  V a l i d ( α ( t ) ) コ Q

1 

( α ( t )

， 

i ) ]   E  TRUE 

となる(定理の証明は，代数的仕様における検証支援系[3Jを用いて行った

[5.6J)。これらの定理を

6.  3  .2 .  3

で、述べた方法に従ってテンポラルロジック の式に変換すると，

[ 1 ] 

¥ l iEI [SEQ ト口 {Q

1 

[ i ] コ

ok

TRANSMES}] 

[  2  ]  ¥ l iEI 

[SEQ  1 =

口

{Q 1 

[i] 

AND  0  l a s t   TRANSMES

コ

OQ 2 

[i]}]  [ 3 ] 

¥ l iEI 

[SEQ 

¹二口

{Q 1 

[i] 

AND  NOT(O l a s t   TRANSMES) 

コ

OQ1 

[i]}] 

のようになる。 (2)‑(5)についても同様に行い，

3 4

個のテンポラルロジックの 式を得るが，その詳細は割愛する(詳しくは文献

C 5 J

参照〉。

以下，変換された性質を

¥ l iEI [SEQ ド Ah

[i]] 

(1

壬

h

壬

3 4 )

で表し，

Al [ i ]

，…， 

A 3 4  

[i]の論理積を

A[

i]で表す。定義より

¥ l iEI [SEQ ト A[

i]] が成立する。

6.4.4 

①，②の証明の概略

まず，①については，回線に関する仮定を用いず，上述の補題A[1 ]のみを 用いて，

第6章 代数的に記述された通信プロトコルの動的性質の検証 103 

ト

A[1]

コ Q[

1 ] 

を証明した[5へまた，②については，任意の正整数を表す定数 kを導入して，

上述の補題

A[K]

，回線に対する仮定

B[K]

および表

6.  2

の

2 2

個のテンポラ ルロジックの公理(推論則〉を用いて，

ドキュメント内 プロトコルの形式的記述と検証 (ページ 107-112)