2.1 Interface Consistency

  This section illustrates a few verification techniques for rigorously checking that different modules have a consistent view of their common interface. A prerequisite for any kind of checking is to have a specification to check against. An interface specification of a component is a rigorous but possibly partial definition of a components interface. By allowing an interface to be partially specified, one leaves it to the designer to decide what should be rigorously defined in the interface specification. The rigor makes it possible to decide whether different components have a consistent view of their common interface.

Traditional compilers make syntactical checks ensuring that the number and type of parameters are consistent. However, it is also important to avoid semantic inconsistencies such as one module assuming one protocol, for example, that a high value of a particular value means ``go'', while another module assumes a different protocol, e.g., that a high value means stop.

As an illustration consider two components X and Y with a common interface. Assume that I_X is a predicate that is satisfied by all the manipulations of the common interface done by module X. Similarly, I_Y is a predicate characterizing the interface manipulations done by Y. In case of the simple arbiter discussed in section 2 such an interface predicate could be $\mbox{$\neg$}{}\; (grant_X \; \mbox{$\wedge$}{} \; grant_Y)$.In this simple example both components have the same predicate so they are obviously consistent. However, in general the predicates can be different which raises the possibility of inconsistency.

In addition to manipulations of the interface, a module may do local modifications. Assume that P_X and P_Y are predicates characterizing these. This means that all changes in module X must satisfy both: $P_X\; \mbox{$\wedge$}{}\;\; I_X$ (and similarly for Y). If $P_X\; \mbox{$\wedge$}{}\;\; I_X$is strong enough to conclude that I_Y holds, and similarly if $P_Y\; \mbox{$\wedge$}{}\;\; I_Y$ is strong enough to conclude that I_X holds, then we may conclude that neither module violates the others requirements on the interface. Hence, interface verification consists of showing two implications such as:

$$P_X\; \mbox{$\wedge$}{}\;\; I_X \Rightarrow I_Y$$

$$P_Y\; \mbox{$\wedge$}{}\;\; I_Y \Rightarrow I_X$$

This sufficient condition is discussed in further detail in [SM95]. Note that this is a weaker condition than requiring equivalence (or equality), hence the term interface consistency.

The expressiveness of the notation used for the predicates is a key issue. In the condition stated above, it was not explicitly stated how to write the predicates characterizing an interface, e.g., I_X. It could be a very restricted notation such as predicate logic with terms consisting only of program variables and constants or one could imagine higher-order logics allowing powerful quantifications. Another interesting possibility is to allow interface predicates to include temporal properties [PG97,RS94]. It is, however, not clear that notations which are very expressive from a theoretical viewpoint are also the most useful in practice. It is my experience that limited notations are often the ones giving the best results in practice, both because they are easier to master and because they allow more efficient tools to be constructed.