Interface Synthesis and Verification

Roberto Passerone, Jerry Burch1, and Luca de Alfaro2
(Professors Alberto L. Sangiovanni-Vincentelli and Thomas A. Henzinger)

Composing intellectual property blocks is an essential element of a design methodology based on re-use. The composition of these blocks when the IPs have been developed by different groups inside the same company, or by different companies, is notoriously difficult. Design rules in the form of interface specifications have been proposed which try to alleviate the problem by forcing the designers to be precise about the behavior of the individual components, and to verify this behavior under a number of assumptions about the environment in which they have to operate. In this work we study the problem of the specification, synthesis, and verification of interfaces for different models of computation and across models of computation. This work supports the Metropolis Meta-Model in the construction of a system integration platform that can integrate heterogeneous models.

Roughly speaking, two agents are compatible if they fit together as they are. In this work we formalize this notion by introducing, for each model of computation, a set of agents that “behave well,” and by deriving a refinement ordering that represents substitutability, called the conformance ordering. We show that under certain assumptions we can represent the set of compatible agents by a single maximal environment, called a mirror. Two agents are compatible if one conforms to the maximal environment of the other.

When components are taken from legacy systems or from third-party vendors, it is likely that their interface communication protocols are not compatible. In this case, an additional adapter can sometimes be introduced to convert from one agent to the other so that their composition is compatible. The notion of a maximal environment allows us to formulate a synthesis algorithm for an adapter that conforms to the specification of a desired communication.

We formulate the problem in particular for synchronous and asynchronous systems. We use an automata-based and a game-theoretic based approach to solving the adaptation problem and to synthesize a converter between two specified protocols.

[1]
R. Passerone, J. A. Rowson, and A. L. Sangiovanni-Vincentelli, "Automatic Synthesis of Interfaces between Incompatible Protocols," Proc. Design Automation Conf., San Francisco, CA, June 1998.
[2]
R. Passerone, L. de Alfaro, T. A. Henzinger, and A. L. Sangiovanni-Vincentelli, "Convertibility Verification and Converter Synthesis: Two Faces of the Same Coin," Proc. Int. Conf. Computer Aided Design, San Jose, CA, November 2002.
1Outside Adviser (non-EECS), Cadence Berkeley Laboratories
2Professor, UC Santa Cruz

Send mail to the author : (roby@eecs.berkeley.edu)


Edit this abstract