この規格 プレビューページの目次
※一部、英文及び仏文を自動翻訳した日本語訳を使用しています。
B.1 はじめに
LOTOS の正式なモデルは、LOTOS 仕様の分析のための厳密な数学的基礎を提供します。この基礎により、この形式モデルに適用できるという条件で、関連する数学的理論のみを使用して仕様の特性を調べることができます。
代数変換の法則により、意味を変えることなく式の部分式を同等の式に置き換えることができます。このような法則は、代数仕様の分析を簡素化します。 LOTOS 仕様の分析では、このアプローチは動作表現と値表現 (ACT ONE 用語) の両方に適用できます。この附属書では、動作表現の変換法則のみが考慮されます。動作表現の検証に関するその他の作業、および抽象データ型の検証に関する作業は、この附属書の参考文献に記載されています。
代数法則を使用して、動作表現は、置換を繰り返すことにより、さらに同等の表現に変換できます。この方法は、システムの 2 つの記述が同等であることを示すために適用できます。たとえば、1 つの記述が元の仕様であり、もう 1 つの記述が実装の LOTOS の記述である場合があります。他の記述は、いくつかの特性をより容易に検証できるシステムの動作のより明確な記述である場合もあります。
B.2 節と B.3 節では、LOTOS 動作表現の変換法則が与えられています。これらの法則は、ラベル付けされた遷移システムを特定することによって達成されます。これは、閉じた動作表現の正式な解釈であり、そのような遷移システムに対して定義された特定の等価関係に従います。 B.2 節と B.3 節で使用される等価関係はどちらも、観察可能な振る舞いを区別できない遷移システムに関連しています。つまり、そのようなシステムを観察 (= 相互作用) することによって、実験者は 1 つのシステムと同等のシステムを区別することができません。
B.2 節と B.3 節で使用される同値関係は、それぞれ「弱いバイシミュレーションの同値」と「テストの同値」と呼ばれます。それらは、「観察可能な同等性」の概念が形式化される方法が異なります。 「弱いバイシミュレーションと同等」である 2 つの式は「テストと同等」でもありますが、その逆ではありません。言い換えれば、「バイシミュレーション」の形式化は、「テスト」よりも多くのシステムを区別します。これら 2 つの同等性の概念のどちらを選択するかは、変換法則を使用したい人が行う必要があります。これは、どちらの関係が識別の技術的基準を最もよく反映しているかに依存します。
残念ながら、弱いバイシミュレーション関係もテストの等価性も、すべてのコンテキストで上記の LOTOS 動作式の置換プロパティを持っていません。独立したシステムと見なした場合、同等の動作表現がありますが、より大きなシステムの一部である場合は異なる動作をします. これは、たとえば、選択表現のコンポーネントを形成する場合に発生する可能性があります.
したがって、完全な置換プロパティを持つ動作表現間のより強い関係が必要です。このような関係は合同関係と呼ばれます。 B.2.2 節と B.3.2 節には、それぞれバイシミュレーション合同関係とテスト合同関係の法則が含まれています。
この附属書の後続の部分に示されている法則のセットは「完全」ではありません。つまり、2 つの式が特定の等価/合同関係にある場合、これは、関連するセットを使用して一方の式を他方の式に変換できることを意味するものではありません。法律の。もちろん、逆の含意も成り立ちます。一連の法則は「健全」です。
B.1 Introduction
The formal model of LOTOS provides a rigorous mathematical basis for the analysis of LOTOS specifications. This basis enables the properties of specifications to be studied by using only relevant mathematical theory, provided that it can be applied to this formal model.
Algebraic transformation laws enable subexpressions of expressions to be replaced by equivalent expressions without change of meaning. Such laws simplify the analysis of algebraic specifications. In the analysis of LOTOS specifications this approach can be applied both to the behaviour expressions and value expressions (ACT ONE terms). In this annex only the transformation laws for behaviour expressions will be considered. More work on the verification of behaviour expressions, and work on the verification of abstract data types can be found in the references of this annex.
Using algebraic laws behaviour expressions may be transformed into further equivalent expressions by repeated substitution. This method may be applied to demonstrate that two descriptions of a system are equivalent. For example one description might be the original specification and the other a description in LOTOS of the implementation. The other description might also be a more explicit description of the behaviour of the systems of which some properties can be more readily verified.
In clauses B.2 and B.3 transformation laws are given for LOTOS behaviour expressions. These laws are attained by identifying labelled transition systems, being the formal interpretation of closed behaviour expressions, following certain equivalence relations that are defined over such transition systems. The equivalence relations used in clauses B.2 and B.3 both relate transition systems that have indistinguishable observable behaviour, i.e. by observing (=interacting with) such systems an experimentor is unable to distinguish one system from an equivalent one.
The equivalence relations used in clauses B.2 and B.3 are termed 'weak bisimulation equivalence' and 'testing equivalence', respectively. They are different in the way in which the concept of 'observable equivalence' is formalized. Two expressions that are 'weak bisimulation equivalent' are also 'testing equivalent', but not vice versa. In other words, the formalization of 'bisimulation' distinguishes between more systems than 'testing'. The choice between these two concepts of equivalence must be made by those who wish to use the transformation laws, depending on which relation reflects their technical criteria for identification best.
Unfortunately, neither the weak bisimulation relation nor the testing equivalence possess the substitution property on LOTOS behaviour expressions described above in all contexts. When considered as systems in isolation there are behaviour expressions that are equivalent, but which will behave differently when they are part of a larger system. This may occur, for example, if they form a component of a choice expression.
Therefore, stronger relations between behaviour expressions are required that do have the full substitution property. Such relations are termed congruence relations. Clauses B.2.2 and B.3.2 contain the laws for the bisimulation congruence relation, and the testing congruence relation, respectively.
The sets of laws that are presented in the subsequent parts of this annex are not 'complete', i.e. if two expressions are in a certain equivalence/congruence relation, this does not imply that one expression can be transformed into the other using the relevant set of laws. Of course, the converse implication does hold: the sets of laws are 'sound'.