Specifying telephone systems in LOTOS

A method for detecting feature interactions in the design of telephone systems using LOTOS (language of temporal ordering specifications) is described. The specification discussed includes call forwarding on a busy line, setting a three-way call, and call waiting. The ways in which a specification of a telephone system involving such features can be constructed in LOTOS and the ways in which LOTOS tools can be used to detect unwanted interactions of the features are illustrated using simple examples. The techniques used are step-by-step execution, symbolic execution, and compositional execution with test processes.<>