/

ISO 8807:1989 情報処理システム—オープンシステム相互接続— LOTOS —観察行動の時間的順序に基づく正式な記述手法 | ページ 7

※一部、英文及び仏文を自動翻訳した日本語訳を使用しています。

B.3 テストの同等性

B.3.1 定義

Sys = < S , A , T , s0 > をラベル付き遷移系とする。

S ∊ Sとすると、 t ∊ ( A -{ i})* に対する集合 ( s after t ) ⊆ Sはs after t ={ s '| によって定義されます。 s = t ⇒ s '}

L ⊆ A -{ i} とすると、述語 ( s must L ) は s must L によって定義されます。 s must L iff s =ε⇒ s ' は、あるa ∈ Lに対してs ' = a ⇒ s " を持つs " が存在することを意味します。

RsSとsと、 R ( R must L ) は 次LLに定義されR 。

Sys1 = < S1 , A1 , T1 , s01 > およびSys2 = < S2 , A2 , T2 , s02 > とし、それらをラベル集合A = A1 ∪ A2に拡張します。述語 ( Sys1 red Sys2 ) は次のように定義されます。

Sys1赤Sys2 iff

( S02 after t ) must Lは ( s01 after t ) must L for every t ∊ ( A -{ i ))* for every L ⊆ ( A -{ i}) を意味します

クローズド LOTOS 動作表現 S B1 、 B2の場合、代数仕様と完全なプロセス環境のコンテキストでは、 B1 赤 B2は、7.5.4 で定義されているように、それぞれの遷移システムSys1 、 Sys2について、 Sys1 赤 Sys2 .

{ x1 , ... , x n} に含まれるすべての自由値識別子を持つ LOTOS 動作表現B1 、 B2の場合B1 赤 B2 iff

[ E1/ x1 , ... E n/ x n ] B1 赤 [ E1/ x1 , ..., E n/ x n ] B2すべてのE1 , ... , E n ,ここで、 E1 、...、 E nは、それぞれx1 、...、 x nと同じ種類の閉値式です。

2 つの LOTOS 動作式B1 、 B2は、 B1 red B2とB2 red B1の場合に同等のテストを行っています。

LOTOS 動作表現の場合B1 、 B2B1 cred B2 iff すべての LOTOS コンテキストの場合C [ ] C [ B1 ] 赤 C [ B2

2 つの LOTOS 動作式B1 、 B2は、 B1 cred B2およびB2 cred B1の合同をテストしています。

B.3.2 合同性をテストする法則

合同性と同等性をテストするための法則は、それらを生成する予約注文の cred と red で表現されます。その理由は、cred と red はそれ自体が興味深いからです。 B1 赤 B2は、 B1がB2の (決定論的) 還元であるという事実を表しています。つまり、 B1はB2よりも非決定論的ではありません。つまり、 B1は環境との相互作用 (テスト) にB2が応答するように応答するため、 B1 赤 B2は「 B1がB2を実装する」と解釈できます。したがって、 赤 は、仕様B2の有効な実装B1のクラスを特徴付けるために使用できます。 cred は、LOTOS コンテキストに関して置換プロパティを持つ red の最大のサブリレーションです。

  • 1) |- B1 = B2はB1 信用 B2を意味する

    注 —これは、cred が B.2.2 に記載されているすべての法則を継承することを意味します。

  • 2)B クレド i ;B
  • 3)g ;( B1 [] B2 ) 信用 g ; B1 [] g ; B2
  • 4)g ; B1 クレジット g ; B1 [] g ; B2
  • 5)B1 cred B2 & B2 cred B3は、 B1 cred B3を意味します。
  • 6)B1 cred B3 & B2 cred B3は ( B1 [] B2 ) cred B3を意味します。

B.3.3 同等性をテストするための法則

  • 1)B1 ≈ B2は、 B1 赤 B2を意味します。
  • 2)C [ ] を次の形式の LOTOS コンテキストとする:
    • a)g ;[ ]
    • b) [ ]|[ A ]| B 、またはB |[ A ]|[ ]
    • c) [ ] >>* B 、またはB >>* [ ]
    • d) [ ][ > B
    • e) [ E ] -> [ ]
    • f) [ ][ S ]
    • g) let ... in [ ]もしB1 赤 B2 then C [ B1 ] 赤 C [ B2 ]

  • 3)B1 赤 B2 & B2 赤 B3はB1 赤 B3を意味します

  • 4)B1 赤 B2 & B2 赤 B3は ( B1 [] B2 ) 赤 B3を意味します

B.3 Testing equivalence

B.3.1 Definitions

Let Sys = < S,A,T,s0 > be a labelled transition system.

Let S ∊ S, then the set (s after t) ⊆ S, for t ∊ (A-{ i})* is defined by s after t ={s'| s = t⇒ s'}

Let L ⊆ A-{ i}, then the predicate (s must L) is defined by s must L iff s =ε⇒s' implies that there exists an s" with s' =a⇒ s" for some a ∈ L

Let R ⊆ S, then the predicate (R must L) is defined by R must L iff s must L for all s ∈ R

Let Sys1 = < S1,A1,T1,s01 > and Sys2 = <S2,A2,T2,s02 >, and extend them to the label set A = A1 ∪ A2, then the predicate (Sys1 red Sys2) is defined by

Sys1 red Sys2 iff

(S02 after t) must L implies (s01 after t ) must L for every t ∊ (A-{ i ))* for every L ⊆ (A-{ i})

For closed LOTOS behaviour expressions SB1, B2, in the context of an algebraic specification and a complete process environment, B1 red B2 iff for their transition systems Sys1, Sys2 respectively, as defined in 7.5.4, Sys1 red Sys2.

For LOTOS behaviour expressions B1,B2 with all their free value-identifiers contained in{x1, ... ,xn} B1 red B2 iff

[ E1/x1, ... En/xn ]B1 red [ E1/x1, ..., En/xn ]B2 for all E1, ... ,En , where E1, ... ,En are closed value expressions of the same sort as x1, ..., xn , respectively.

Two LOTOS behaviour expressions B1,B2 are testing equivalent iff B1 red B2 and B2 red B1.

For LOTOS behaviour expressions B1,B2B1 cred B2 iff for all LOTOS contextsC [ ] C [ B1 ] red C [B2 ].

Two LOTOS behaviour expressions B1,B2 are testing congruent iff B1 cred B2 and B2 cred B1.

B.3.2 Laws for testing congruence

The laws for testing congruence and equivalence will be expressed in the pre-orders cred and red that generate them. The reason for this is that cred and red are interesting in their own right. B1 red B2 expresses the fact that B1 is a (deterministic) reduction of B2, i.e. B1 is less nondeterministic than B2. Since this reduction leaves deadlock properties intact, i.e.B1 responds to interactions with the environment (tests) as B2 might respond,B1 red B2 can be interpreted as 'B1 implements B2'. red may thus be used to characterize the class of valid implementations B1 of a specification B2. cred is the largest sub-relation of red that has the substitution property with respect to LOTOS contexts.

  • 1) |-B1 = B2 implies B1 cred B2

    NOTE — This implies that cred inherits all the laws listed in B.2.2.

  • 2)B cred i ;B
  • 3)g;(B1 [] B2) cred g;B1 [] g;B2
  • 4)g;B1 cred g;B1 [] g;B2
  • 5)B1 cred B2 & B2 cred B3 implies B1 cred B3
  • 6)B1 cred B3 & B2 cred B3 implies (B1 [] B2) cred B3

B.3.3 Laws for testing equivalence

  • 1)B1 ≈ B2 implies B1 red B2
  • 2) Let C[ ] be a LOTOS context of the following forms:
    • a)g;[ ]
    • b) [ ]|[ A ]| B, or B|[ A ]|[ ]
    • c) [ ] >>* B, or B >>* [ ]
    • d) [ ][ > B
    • e) [ E ] -> [ ]
    • f) [ ][ S ]
    • g) let ... in [ ]then if B1 red B2 then C [ B1 ] red C[ B2 ]

  • 3)B1 red B2 & B2 red B3 implies B1 red B3

  • 4)B1 red B2 & B2 red B3 implies (B1 [] B2) red B3

ISO PDF プレビュー