‑AXIO) 。

p r e f i x  a c

tI 

( n

， j 

1

， j 

2  ) 

局

n

の

ISEQ

の

1

番目から j

2 

(孟 j

1 

)番目までのパケット系列 Sが， j 

1

番目のパケットから始まるアクティブ受信部に属しているか否かを表す述 語である。すなわち

s

がトークンで始まり最終フレームで終るアクティプ受 信部の初期部分系列であるときに真となる述語である。

p r e f i x  actO ( n

， 

k  1

， 

k  2  ) 

局

n

の

OSEQ

の

kl

番目から

k2(

と

k1)

番目までのパケット系列 S

が， k 1番目のパケットから始まるアクティプ受信部に属しているか否かを表 す述語である。すなわち

s

がフレームで始まり O個以上のフレームが続いた 後トークンで終るアクティブ送信部の初期部分系列であるときに真となる述語 である。

c o m p l e t e  a c

tI 

( n

， j 

1

， j 

2  ) 

局

n

の

ISEQ

のj

1

番目から j

2

番目までのパケット系列が， j 

1

番目の パケット(トークン)から始まり j

2

番目のパケット(最終フレーム〉で完了す るアクティプ受信部であるときに真となる述語である。

c o m p l e t e  actO ( n

， 

k  1

， 

k  2  ) 

局

n

の

OSEQ

の

kl

番目から

k2

番目まで、のノミケット系列が，

k  1

番目

112  第7章 代 数 的 手 法 の ト ー ク ン リ ン グ 方 式LANへの応用 表7. 1 局の仕様

SPEC ST A TION (n)  ; 

Project PRIMITIVES ; {基底代数を使用する宣言}

{関数の宣言部}

OP  nn integer → station num I packet num ;  nn integer → lengthI (station num) ; 

→ lengthO(station num) ; 

types  → typlI(station num， packet num) ; 

→ typeO(station num， packet num) ;  data  → contentI(station num， packet num) 

→ contentO(station num， packet num) 

bool → prefix  actI(station num， packet num， packet num) ; 

→ prefix actO(station num， packet num， packet num) 

→ complete actI(station num， packet num， packet num) 

→ complete actO(station num， packet num， packet num) 

→ frame seqI(station num， packet num， packet num) 

→ equal(station num， packet num， packet num) 

→ match(station num， packet num， packet num)  nn integer → max matchI (station num) 

→ max matchO(station num) ;  {変数の宣言部)

station num n ; 

packet num j， jl， j2， k， kl， k2， p， q ;  {公理の宣言部}

AX 1 :  prefix  actl(n， j 1 . j 2 )  (j  2 ~玉 lengthI(n)) and 

[{ (j 1 = j 2) and typel(n， j 2 )二token}or  { (j  1 < j 2) and prefix  actI (n， j 1 ， j 2 ‑ 1) and 

(typeI(n， j 2) =last or typeI(n， j 2) =intermediate)  and (typeI (n， j 2 ‑ 1 ) = intermediate or 

typeI(n， j 2 ‑1 ) = token) } ] ;  AX 2 :  prefix  actO(n， k 1 ， k 2 ) 

(k 2 ~玉 lengthO(n)) and 

{(k 1 = 1 ) or not(prefix  actO(n， k 1 ‑ 1， k2))}  and  [{ (k 1 = k 2) and (typeO(n， k 2 ) = intermediate or 

typeO(n， k 2 )二last)}or  [(k 1 <k 2) and prefix  actO(n， k 1， k 2 ‑ 1) and 

{(typeO(n， k 2 ) = intermediate and 

第7章 代数的手法のトークンリング方式LANへの応用 113  表7.1 局の仕様(前頁より続く〉

typeO(n， k 2 ‑ 1) =intermediate) or  (typeO(n， k 2) =last and 

typeO(n， k 2 ‑ 1 ) = intermediate) or 

(typeO(n， k 2 ) = token and typeO(n， k 2 ‑ 1) = last)}]]  ;  AX 3 :  complete actI(n， j 1， j 2 ) 二 二

prefix actl (n， j 1 ， j 2) and typel (n， j 2 ) = last ;  AX 4 :  complete actO(n， k 1 ， k 2 ) 二 =

prefix actO(n， k 1 ， k 2) and typeO(n， k 2 ) =token ;  AX 5 :  frame seql (n， j 1 ， j 2 ) 二 二

(j 2壬lengthl(n)) and 

{typel (n， j 2 ) = last or typel(n， j 2 ) = intermediate}  and  { (j 1 = j 2) or ((j 1 

< 

j 2) and frame seq I (n， j 1 ， j 2 ‑ 1 ))} ;  AX 6 :  equal(n， j， k)二 二

(j三五lengthl(n)) and (k壬lengthO(n))and  typel(n， j) =typeO(n， k) and 

{typel (n， j) = token or contentl (n， j)ニcontentO(n，k)} ;  AX 7 :  match(n， 0， 0)二 二 TRUE;

AX 8 :  match(n， p， q)コ

[{ (complete actI(n， p+ 1， j) and complete actO(n， q+ 1， k))  or ((j=p+ 1) and (k二q+ 1) and equal(n， j， k))}コ match(n， j， k)]二 二 TRUE;

AX 9 :  match(n， max matchl(n)， max matchO(n))二 二 TRUE;

AX 10:  [{ (pミmaxmatchl(n) and q>max matchO(n)) or  (p>max matchl(n) and qミmaxmatchO(n))} and  match(n， p， q)]二 二 FALSE;

AX 11:  [lengthl(n) =max matchl(n) or 

frame seql(n， max matchl(n)十1， lengthl (n)) or  {frame seql (n， max matchl (n)十1， lengthl (n) ‑ 1 ) and 

typel(n，lengthl(n))二tokenand  typel(n， lengthl(n) ‑ 1) =last}]コ lengthO(n) =max matchO(n)二 二 TRUE;

AX 12:  [{(max matchl(n)= 0) or typel(n， max matchl(n))=last or 

END; 

typel(n， max matchl(n))=token} and  prefix actl(n， max matchl(n)+ 1， lengthl(n))]コ {prefix actO(n， max matchO(n)+ 1， lengthO(n)) or  lengthO(n)二maxmatchO(n)}  = = TRUE ; 

114  第7章 代数的手法のトークンリング方式L A Nへの応用

のパケットから始まり k2番目のノミケット(トークン)で完了するアクティプ 送信部であるときに真となる述語である。

frame s e q I ( n

， j 

1

， j 

2) 

局

n

の

ISEQ

のj

1

番目のノミケットから j

2

番目のノミケットまでのすべ てのパケットがフレームであるときに真となる述語である。

e q u a l  ( n

， j， 

k )  

局

n

の

ISEQ

のj番目のパケットと

OSEQ

の

k

番目のノミケットの型が 等しく，フレームの場合はさらに内容も等しいときに真となる述語である。

match(n

， 

p

， 

q )  

局

n

において

ISEQ

の

p

番目のパケットおよび

OSEQ

の

q

番目のノミ ケットが対応する構成単位の最後のノミケットであるときに真となる述語である。

max match I ( n )  

(または

maxmatchO ( n ) )  

match(n

， 

p

， 

q )

を満たす

p

(または

q )

の最大値である。

中継局および発信局の仕様は，上述の関数および述語を用いて，その入出力 系列の対応を記述することによって与えられる(表

7. 

1 、 AXll~AX12) 。 AXll~AX12 は，

ISEQ

および

OSEQ

のそれぞれが，

max match 1  ( n )

およ び

maxmatchO ( n )

よりも上の部分に対する記述であり，

max match 1  ( n )

お よび

maxmatchO ( n )

よりも上には抽出できる構成単位はないと記述されて いる。

(1)  中継局

n(AXll) 

次のいずれかが成立するならば，局

n

の

OSEQ

の長さは

maxmatchO(n) 

でなければならない。

(a) 

ISEQ

の長さが

maxmatch 1  ( n )

で、ある。

(b) 

ISEQ

の

(maxmatch 1  ( n )   +  1 

)番目のノ4ケットから

ISEQ

の最後 (l

e n g t h   1  ( n )

番目〉のパケットまですべてフレームである。

(c) 

ISEQ

の

(maxmatch 1  ( n )   +  1 

)番目のノミケットから

ISEQ

の最後か ら

2

番目のノミケットまですべてフレーム，特に最後から

2

番目のノξケッ

トが最終フレームであり，最後のノミケットがトークンである。

この (a)は中継局が最後に受信したノミケットを中継した状況を， (b)は受信し

第7章 代 数 的 手 法 の ト ー ク ン リ ン グ 方 式L A Nへの応用 115  t r一一寸 Horizontal line indicates locations 

d一寸 of max matchl(n)  and max matchO(n) 

n

門

fO

円

^{t : Token} 

1 1 1   1  1 1 1   1  1 1 1   1  ~O: ~;::::=

^{f印o: Intermediate frames more than or} 

ISEQ  OSEQ  ISEQ  OSEQ  ISEQ  OSEQ  equal tω00 

(a)  State 1  (b) State 2  (c) State 3  fl: Frames more than O(only uppermost  frame can be a last frame)  a， b : Intermediate frames 

凸 り

︐&'A l 

r +E A  

ISEQ  OSEQ  ISEQ  OSEQ  ISEQ  OSEQ  ISEQ  OSEQ  ISEQ  OSEQ  (d) State 4  (e) State 5  (f) State 6  (g) State 7  (h) State 8 

図7.3 表7.2の 仕 様 を 満 た す ISEQとOSEQ

たいくつかの中継すべきフレームを未だ送信していない状況を， (c)は(b)の状 況に加えてさらにトークンまで受信している状況を表しており，それぞれ，図

7 . 3 (a)から図7. 3 (c)に対応する。

(2)  発信局 n (AX12) 

局

n

において，

max match 1  ( n )   =  0

で

ISEQ

が空であるか

maxmatch 1  ( n )

番目のノ〈ケットが中間フレームでないかのいずれかであり，かつ，

(max  match I ( n )

十

1

)番目のパケットから

ISEQ

の最後のパケットまでが一つのア

クティプ受信部の初期部分系列であるならば，

OSEQ

の

(maxmatchO(n)

^十

1)

番目のノミケットから

OSEQ

の最後のパケットまでが一つのアクティプ送信 部の初期部分系列(空系列を含む〉でなければならない。これは， トークンを 受け取って発信局となった局が，零個以上の一連のフレームを発信し，一巡し てきたそれらのフレームをアクティブ受信部として受け取る状況を表しており，

その状況は図

7.  3 

(d)から図

7.  3 

(g)のように場合分けできる。また，

ISEQ

の

(max match I ( n )   +  1)

番目のノfケットから上の系列がでたらめであるなら ば，局 nは何を出力しでもよい(図7. 3 (h))。

上述の局

n

の仕様を

ST

A 

TION  ( n )  

"と呼ぶ(表7. 1)0  AX12では，簡

116  第7章 代数的手法のトークンリング方式LANへの応用

単のため，発信局がまだ出力していないフレームを，先に(リングを一周して〉

受け取ったかのような状況も許しているが，これは単に

l e n g t hI ( n )

豆

l e n g t h O

(n)とL、う制約を記述していないに過ぎない。すなわち，この仕様は，検証した い性質の検証に必要な要求の記述のみから成っており，その意味において仕様 の記述はなるべく緩いものとなっている。なお， リング全体が

7.  2  .  2

で述べ る仕様を満たしつつ，特定の初期状態(後述〉より出発して動作するならば図 7 . 3 (a)~(g) の 7 つのうちのいずれかになることは後述の検証作業の一部とし

て証明されている。

7.2.2 

リング全体の代数的仕様

リング上の局の数を

N

とする。各

n( 1

壬

n

豆

N)

について

n

番目の局の 入力パケット系列および出力パケット系列をそれぞれ

ISEQn

および

OSEQn

と表す。

N

個の局の仕様

STATION(n)"( 1  

~玉 n 壬 N) を部分仕様として含む

表7. 2 リング全体の仕様 SPEC  RING(N) ; 

For k : = 1 to N do {INCLUDE STATION(k)} ;  OP  station num→N 

station num n  packet num j 

AX 1 :  lengthI( 1 )孟1^{二 =}TRUE; 

AX 2 :  typel( 1， 1) =token = = TRUE; 

AX 3 :  (n^主主2 ) コlengthO (n ‑1 )註lengthI(n)= = TRUE ;  AX 4 :  {(n孟2)and j壬lengthl(n)}コ

[typeO(n‑1， j)二typeI(n， j) and 

{typeI (n， j) = token or contentO(n ‑1 ， j)二contentI(n， j)} ] 

二 二 TRUE;

AX 5 :  lengthO(N)十1ミlengthI(1 )二二 TRUE;

AX 6:  (2壬j壬lengthI(n) )コ

END; 

[typeO(N， j‑1 ) = typeI ( 1， j) and 

{ typeI ( 1 ， j)二tokenor contentO (N， j ‑1 ) = contentI ( 1 ， j) } ] 

二 二 TRUE;

第7章 代数的手法のトークンリング方式LANへの応用 117  リング全体の仕様を

RINGCN)"

で表す(表

7.2)

。

RINGCN)"

は，各局の仕様，および

ISEQ 1

， 

OSEQ  1

， 

ISEQ  2

， 

OSEQ  2

，…， 

ISEQN

， 

OSEQN

聞において満たされるべき関係として記述される。

(1) 

N

個の局の仕様:各

nC 

1豆

n

孟

N)

に対し，

ISEQn

および

OSEQn

は

7  .  2  .  1

に示した局の仕様を満たさなければならなし、。

RINGCN)"

において は，すべての局の仕様を含むことによってそのことが明示されている。

(2)  動作の開始:リングは，一つのトークンだけが局1の

ISEQ

の1番目の パケットにある状態(リングの初期状態と呼ぶ〉からその動作を開始すると仮 定して公理が作成されている

CAX 1

， 

AX  2)

。

(3)  隣接する局間の関係:通信媒体上では，誤りは生じないものと仮定し，

通信媒体上で生じる遅延の大きさは任意であると考える。このことは，単に，

局の入力パケット系列は直前の局の出力パケット系列の任意の初期部分系列で あるということで記述される

CAX 3  ‑AX  6)

。ただし，

ISEQ  1

と

OSEQN

の 関係においては，上記の (2)より，

OSEQN

には対応するトークンがないけれ ども

ISEQ 1

の

1

番目のノミケットにはトークンがあると仮定されている

CAX

5， 

AX  6)

。

7.3 

局およびリングの仕様のもつ性質とその検証

7.2

で、述べた局およびリングの仕様は，規格のすべてではなく，局の仕様の うち，それがもっ「安全性」および「相互排他性」とし、う二つの性質を成り立 たせるのに必要な要求のみを記述している。本節では，まず，

7.3. 1

で二つ の性質の記述に必要な補助関数について，

7.3.2

では検証を行うために導入 された記述について説明する。さらに，

7.3.3

および

7.3.4

では検証支援 系を用いて形式的に証明を行ったいくつかの定理について非形式的に説明して いる。

7  . 3  .  1 

性質の記述

まず，二つの性質の記述のため，発信局から発信されたフレームはその内容 を変更することなく下流のある局までか，すべての局かのいずれかに伝達され

1 1 8  

第

7

章 代 数 的 手 法 の ト ー ク ン リ ン グ 方 式

LAN

への応用

ることを表す述語や， リング上にトークンが1個しかないことを表す述語など，

いくつかの補助関数を導入する。これらの関数は，安全性および相互排他性自 身の代数的記述を容易に行ったり，二つの性質が成り立つことの証明を行うた めに必要な関数であり，表

7.3

に示す。以下，主な関数について説明する。

s a m e  ( n

， 

m

， j)  :局

n

の

OSEQ

から下流に向って局

m

の

I S E Q

までのす べての

I S E Q

および

OSEQ

について， j番目(途中に局

1

がある場合は局

1

以 降は (j+1)番目〉のノミケットの型・内容がともに一致しているときに真とな

る述語である。

s a m e  n u l l  ( n

， 

m

， j)  :局

n

から下流の局

m

までの間にある局

p

が存在 し，局

n

の

OSEQ

から局

p

の

I S E Q

または

OSEQ

までのすべての

I S E Q

お よび

OSEQ

のj番目(途中に局

1

がある場合は局

1

以降は (j+

1 )

番目〉の パケットの型・内容がともに一致しており，局 pのそれ以降下流の局 m の

I S E Q

までのすべての

I S E Q

(および

OSEQ)

の長さが j(局

1

よりも下流に ある局についてはj十 1)より短いときに真となる述語である。

t r a n s m i t  ( n

， 

k )  

:発信局

n

の

OSEQ

において，

k

番目のノミケットが，あ るアクティプ送信部に属しているフレームであるとき真となる述語である。

t o k e n  n u m b e r  i n   r i n g ( n

， 

m) 

:局

n

から下流の局

m

までの各局が保持 しているトークン数およびこれらの各局が送信し未だ次局で受信されていない

表7.3 I安全性」および「相互排他性」の検証のために導入した補助関数群

SPEC SAFENESS  &  MUTUAL EXCLUSION ;  INCLUDE R I N G ( N )  ; 

OP 

station num→ inc(station num) 

→ dec(station num) ; 

packet num→ index(station num， station num， packet num) ;  bool → eq rec(station num， station num， packet num) ; 

→ same(station num， station num， packet num) ; 

→ same null(station num， station num， packet num) 

→ transmit(station num， packet num) 

OP 

station num →

N; 

station num n， m ;  packet num j， k， k 1 ， k 2 

第7章 代 数 的 手 法 の ト ー ク ン リ ン グ 方 式LANへの応用 119  表7. 3 

r

安全性」および「相互排他性」の検証のために導入した補助関数群(前頁より続く〉

AX 1 :  inc(n)二二 ifn=N then  1 else n+ 1  AX 2 :  dec(n)二二 ifn二1then N else n‑1  AX 3 :  index(n， m， j) = = if  m>n then j else j+ 1 

{安全性の検証のために導入した公理) SF 1 :  eq rec(n， m， j)二二

if  m二 inc(n)

then lengthO(n)詮jand 

lengthl(m)孟index(n，m， j) and 

typeO(n， j) =typeI(m， index(n， m， j)) and  {typeO(n， j)二tokenor 

contentO(n， j) = contentI (m， index (n， m， j)) }  else lengthO(dec(m))孟index(n，dec(m)， j) and 

lengthI(m)孟index(n，m， j) and  (typeO(dec(m)， index(n， dec(m)， j)) 

=typeI(m， index(n， m， j))) and 

{typeO(dec(m)， index(n， dec(m)， j))=token or  (contentO(dec(m)， index(n， dec(m)， j)) 

二contentI(m， index (n， m， j)))} ;  SF 2 :  same(n， m， j)二二

if  m=inc(n) then eq rec(n， m， j)  else same(n， dec(m)， j) and 

SF 3 :  same null(n， m， j)  if  m=inc(n) 

equal(dec(m)， index(n， dec(m)， j)，  index(n， dec(m)， j))  and eq rec(n， m， j)  ; 

then eq rec(n， m， j) or (lengthI(m) <index(n， m， j))  else  {same null(n， dec(m)， j) and 

lengthO(dec(m)) <index(n， dec(m)， j) and  lengthI (m) < index (n， m， j)} or 

{same(n， dec(m)， j) and 

equal(dec(m)， index(n， dec(m)， j)，  index(n， dec(m)， j)) and  lengthI(m) <index(n， m， j)} or  same(n， m， j)  ; 

SF 4 :  prefix  actO(n， k 1 ， k 2) and k 1孟k孟k2 and typeO(n， k)ヰtoken コtransmit(n，k)二 二 TRUE;

120  第7章 代数的手法のトークンリング方式LANへの応用

表7. 3 I安全性」および「相互排他性」の検証のために導入した補助関数群(前頁より続く〉

{相互排他性の検証のために導入した公理}

OP  integer → token numberI(station num， packet num， packet num) ; 

→ token numberO(station num， packet num， packet num) 

→ token number on line  from(station num) ; 

→ token number at  station(station num) ; 

→ token number in  ring(station num， station num)  M U  1:  token numberI (n， j 1 ， j 2 )二二

if (j 1 > j 2 ) then 0  else if  (typeI(n， j 1) =token) 

then token numberI (n， j 1 + 1 ， j 2 ) + 1  else  token numberI (n， j 1 

+ 

1 ， j 2) ;  M U  2 :  token numberO(n， j 1 ， j 2 )二二

if (j 1 > j 2 ) then 0 

else if  (typeO(n， j 1 )ニtoken)

then token numberO(n， j 1 + 1 ， j 2 ) + 1  else  token numberO(n， j 1 + 1 ， j 2) ;  M U  3 : token number at station(n) 二

if  token numberI(n， max matchI(n)十1，lengthI(n))ミ token numberO(n， max matchO(n) + 1， lengthO(n))  then token numberI (n， max matchI (n) + 1 ， lengthI (n)) 

‑ token numberO(n， max matchO(n) + 1 ， lengthO(n))  else 0 ; 

M U  4:  token number on line  from(n)二二 if  (n<N) 

then token numberO(n， lengthI(n十1) + 1 ， lengthO(n))  else  token numberO(N， lengthI( 1)， lengthO(N)) ;  M U  5 :  token number in  ring(n， m) 二

END; 

if  (n二m)then token number at station(n) + 

token number on line  from(n)  else  token number at  station(n) + 

token number on line  from(n) + 

token number in  ring(inc(n)， m) ; 

第7章 代 数 的 手 法 の ト ー ク ン リ ン グ 方 式LANへの応用 121 

7.3.2 

検証のための記述

表

7 . 2

で与えた局およびリングの仕様では，各局の入出力系列の構成や入出 力系列聞に成立しなければならない関係についてのみ記述してあり，表

7.2

の公理系を満たす入出力系列対(関数〉については安全性を表す

r t r a n s m i t ( n

，

k ) コ samen u l l  ( n

， 

n

， 

k )   J

や相互排他性を表す

r token number i n   r i n g (  1 

，  N)= 1 

J

は(表

7.3

の公理系では〉成立しなし、(後述の図

7.4

参照〉。証明し たいことは，初期状態(局

1

の

I S E Q

にトークンが

1

個だけある状況〉から出 発して，表

7 . 2

の公理を満たすようにパケットを追加(すべての局の

I S E Q

，

OSEQ

の長さの総和が

1

増加〉していったときの状態において，安全性や相互 排他性が成り立つということである(+)。そのことを代数的に議論するために，各 関数の引数を一つ増やし，

r

状態」を引数に含める。

表

7.4

は，表

7.3

にリング全体の状態を表すソート

s t a t e

を新たに導入し たものであり，表

7.5

は状態の推移に関する公理を表

7.4

に加えたものであ る。

I N I T I A L

はリングの初期状態を表す。状態 xにおいて，ある局の入力系 列または出力系列に任意に一つだけパケットを追加した任意の状態 yを

n e x t ( x )

で、表し，このとき，しかもこのときのみ真となる述語を

r e a c h ( x

，y)とす る。 リング全体の状態は初期状態から出発して任意の回数だけ関数

n e x t "

を 施して得られる状態であり，具体的にパケットの追加の仕方を順次特定すると 全ての局の入出力系列対が定まる。各関数fに対して， f. 

s

は状態Sにおける 関数 fを表しており， t. 

s

は項

t v

こ含まれる各関数f，

g

， 

h

， … を f.

s

， 

g .   s

，  h. 

s

，…で置き換えて得られるものであり状態Sにおける項

t

を表している。

s u m l e n g t h .  s 

， (i j)は，状態Sにおける局

i

から局 jまでの入力系列および出力 系列の長さの総和である。公理

REl‑RE3

は，任意の状態において，任意に

(十) 通常，各局の動作は，パケットの受信と送信に分離され，各局が何かの動作を実行す るごとに，入力ノミケット系列または出力ノミケット系列にパケットが1個追加される。

リング全体では各局のこれらの動作が並行して実行され得るが，以下では便宜上，一 時には1局 の み が 動 作 す る と み な し て 考 察 す る ( こ れ に よ り 本 質 が 失 わ れ る こ と は ない)。

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