This paper develops a semantic theory for heterogeneous system
designs in which some components are specified operationally and
others are given logically. Using the traditional testing paradigm
of DeNicola and Hennessy as a basis, the formalism introduces Buechi
processes and Buechi tests with associated may- and must-preorders.
These refinement orderings are then given alternative
characterizations and shown to be conservative extensions of the
relations studied by DeNicola and Hennessy. The paper also
establishes a tight connection between the Buechi must-preorder and
satisfaction of linear-time temporal logic (LTL) formulas by showing
that a system satisfies an LTL formula if and only if it is larger
than the Buechi process corresponding to the formula in the
must-preorder. Consequently, the Buechi must-preorder permits a
uniform treatment of traditional notions of process refinement and
LTL satisfaction. It also provides an elegant semantic basis for
heterogeneous system designs in which some system components are
specified as labeled transition systems and others as LTL formulas.
An example dealing with the design of a small communications
protocol illustrates this point.
