A behavioral interface automaton (BIA) of a component expresses some aspects of that components run-time (i.e., temporal) behavior. Depending on how much information about temporal behavior is included in the automaton, there is a spectrum of state information ranging from a maximal BIA for the component (which includes every transition the component makes, even internal ones), to a trivial automaton consisting of a single state. Thus, any BIA for a component can be regarded as a homomorphic image of the maximal automaton. This spectrum refines the traditional white-box/black-box spectrum of component reuse, ranging from exporting the complete source code (maximal automaton) of the component--white-box, and exporting just the interface (trivial automaton)--black box. Table 1 displays this spectrum.
In practice, it is unrealistic to expect the programmer to provide the maximal BIA, just as precisely specified semantics are rarely part of programming practices. As long as the most important behavioral properties (e.g., the safety-critical ones) can be expressed and established, a homomorphic image of the maximal automaton (which omits some information on the components behavior) is sufficient (Table 1 middle column).
The BIA can be provided by the component designer and verified by the compiler (just like typed interfaces are) using techniques such as abstraction mappings and model checking. Verification is necessary to ensure the correctness of the BIA, i.e., that it is truly a homomorphic image of the maximal automaton. Alternatively, the component compiler can generate a BIA from the code, using, for example, abstract interpretation or machine learning [15]. In this case, the BIA will be correct by construction. We assume the first option for third party components, and will explore the second option for components assembled in our builder.