Convertibility verification and converter synthesis: two faces of the same coin

ABSTRACT

An essential problem in component-based design is how to compose components designed in isolation. Several approaches have been proposed for specifying component interfaces that capture behavioral aspects such as interaction protocols, and for verifying interface compatibility. Likewise, several approaches have been developed for synthesizing converters between incompatible protocols. In this paper, we introduce the notion of adaptability as the property that two interfaces have when they can be made compatible by communicating through a converter that meets specified requirements. We show that verifying adaptability and synthesizing an appropriate converter are two faces of the same coin: adaptability can be formalized and solved using a game-theoretic framework, and then the converter can be synthesized as a strategy that always wins the game. Finally we show that this framework can be related to the rectification problem in trace theory.

REFERENCES

• 1: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, 1987
• 2: Roberto Passerone , James A. Rowson , Alberto Sangiovanni-Vincentelli, Automatic synthesis of interfaces between incompatible protocols, Proceedings of the 35th annual conference on Design automation, p.8-13, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277047]
• 3: Kanna Shimizu , David L. Dill , Alan J. Hu, Monitor-Based Formal Specification of PCI, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.335-353, November 01-03, 2000
• 4: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 5: Luca de Alfaro , Thomas A. Henzinger, Interface Theories for Component-Based Design, Proceedings of the First International Workshop on Embedded Software, p.148-165, October 08-10, 2001
• 6: Sagar Chaki , Sriram K. Rajamani , Jakob Rehof, Types as models: model checking message-passing programs, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.45-57, January 16-18, 2002, Portland, Oregon
• 7: Alberto L. Sangiovanni-Vincentelli , Marco Sgroi , Luciano Lavagno, Formal Models for Communication-Based Design, Proceedings of the 11th International Conference on Concurrency Theory, p.29-47, August 22-25, 2000
• 8: Felice Balarin , Luciano Lavagno , Claudio Passerone , Alberto Sangiovanni-Vincentelli , Yosinori Watanabe , Guang Yang, Concurrent execution semantics and sequential simulation algorithms for the metropolis meta-model, Proceedings of the tenth international symposium on Hardware/software codesign, May 06-08, 2002, Estes Park, Colorado [doi>10.1145/774789.774793]
• 9: Jerry R. Burch , David Dill , Elizabeth Wolf , Giovanni de Micheli, Modeling hierarchical combinational circuits, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.612-617, November 07-11, 1993, Santa Clara, California, United States
• 10: J. Thatcher and J. Wright, "Generalized finite automata theory with an application to a decision problem of second-order logic," Mathematical System Theory, vol. 2, pp. 57--81, 1968.
• 11: J. Büchi and L. Landweber, "Solving sequential conditions by finite-state strategies," Trans. Amer. Math. Soc., vol. 138, pp. 295--311, 1969.
• 12: W. Thomas, "On the synthesis of strategies in infinite games," in Proc. of 12th Annual Symp. on Theor. Asp. of Comp. Sci., vol. 900 of Lect. Notes in Comp. Sci., pp. 1--13, Springer-Verlag, 1995.
• 13: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 14: Yuri Gurevich , Leo Harrington, Trees, automata, and games, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.60-65, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802177]
• 15: E. A. Emerson , C. S. Jutla, Tree automata, Mu-Calculus and determinacy, Proceedings of the 32nd annual symposium on Foundations of computer science, p.368-377, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185392]
• 16: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Hardware/software interfaces

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Analysis of algorithms

General Terms:
Algorithms, Design, Performance, Theory