Failure-based Congruences, Unfair Divergences and New Testing Theory
English
Leduc, Guy[Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques >]
Jun-1994
Protocol Specification, Testing and Verification, XIV
Vuong, Son
Chanson, Sam
Chapman & Hall
252-267
No
International
London
UK
14th Conf. on Protocol Specification, Testing, and Verification (PSTV)
June 1994
S. Vuong, S. Chanson
Vancouver
Canada
[en] Formal language ; Testing
[en] The testing equivalence 'te' that is used as a reference in verification and testing theory in LOTOS is not a congruence, and no explicit definition of the least congruence stronger than 'te' has been found. The critical LOTOS context in which congruence is lost is the hiding context that creates divergence. In this paper we first survey this problem and present three known variants of 'te' that are congruences. Each of them, as well as 'te', is then related to a particular interpretation of divergences in terms of (un)fairness of divergences. The associated preorders that generate these equivalences are also presented. Based on these results, we propose a new testing theory based on unfair divergences. It defines new equivalence and conformance relations, as well as the associated canonical tester. We also prove that the least congruence stronger than this new testing equivalence is one of three presented failure-based congruences, which thus also deserves the label of testing congruence.
Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS