Specification Enforcing Refinement for Convertibility Verification

Abstract : Protocol conversion deals with the automatic synthesis of an additional component, often referred to as an adaptor or a converter, to bridge mismatches between interacting components, often referred to as protocols. A formal solution, called convertibility verification, has been recently proposed, which produces such a converter, so that the parallel composition of the protocols and the converter also satisfies some desired specification. A converter is responsible for bridging different kinds of mismatches such as control, data, and clock mismatches. Mismatches are usually removed by the converter by disabling undesirable paths in the protocol composition (similar to controllers in supervisory control of Discrete Event Systems (DES)). We generalize this convertibility verification problem by using a new refinement called specification enforcing refinement (SER) between a protocol composition and a desired specification. The existence of such a refinement is shown to be a necessary and sufficient condition for the existence of a suitable converter. We also synthesize automatically the converter if a SER refinement relation exists. The proposed converter is capable of the usual disabling actions to remove undesirable paths in the protocol composition. In addition, the converter can perform forcing actions when disabling alone fails to find a converter to satisfy the desired specification. Forcing allows the generation of control inputs in one protocol that are not provided by the other protocol. Forcing induces state-based hiding, an operation not achievable using DES control theory.
Type de document :
Communication dans un congrès
International Conference on Application of Concurrency to System Design, ACSD'09, Jul 2009, Augsburg, Germany. IEEE, pp.148--157, 2009, 〈10.1109/ACSD.2009.25〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00753172
Contributeur : Alain Girault <>
Soumis le : samedi 17 novembre 2012 - 23:04:52
Dernière modification le : jeudi 11 janvier 2018 - 06:22:03
Document(s) archivé(s) le : lundi 18 février 2013 - 03:42:57

Fichier

acsd09-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Partha Roop, Alain Girault, Gregor Goessler, Roopak Sinha. Specification Enforcing Refinement for Convertibility Verification. International Conference on Application of Concurrency to System Design, ACSD'09, Jul 2009, Augsburg, Germany. IEEE, pp.148--157, 2009, 〈10.1109/ACSD.2009.25〉. 〈hal-00753172〉

Partager

Métriques

Consultations de la notice

244

Téléchargements de fichiers

73