An analysis of relationships between Craig-style interpolation, compactness, and other related model-theoretic properties is carried out in the softer framework of categories of pre-institutions. While the equivalence between sentence interpolation and the Robinson property under compactness and Boolean closure is well known, a similar result under different assumptions (not involving compactness) is newly established for presentation interpolation. The standard concept of naturality of model transformation is enriched by a new property, termed restriction adequacy, which proves useful for the reduction of interpolation along pre-institution transformations. A distinct reduction theorem for the Robinson property is presented as well. A variant of the ultraproduct concept is further introduced, and the related closure property for pre-institutions is shown to be equivalent to compactness

The Language for temporal ordering specification (LOTOS) is a formal description technique whose development is under way within ISO, the International Organization for standardization, mainly for application to open systems interconnection (OSI) standards. The paper presents a LOTOS specification of the PROWAY interface for process control applicatioins, defined by IEC, the International Electrotechnical Commision. LOTOS is shown to be tailored for the specification of asynchronous systems. In particular, it proves suitable for the specification both of the services which define an interface and of the protocols which implement it. The paper shows how LOTOS supports formal reasoning aimed at establishing consistency between service and protocol specifications. Two examples of such a verification are developed that are related to the PROWAY interface. Finally, advantages and limitations of this approach are outlined.