This talk surveys some work on specification of telephone services and detection of feature interactions. We present a framework for the specification of telephone systems in linear-time temporal logic. The framework can be used for specifying both high-level properties, as well as more precise functional behavior of services. Beased on this framework, we present a framework to detect feature interactions automatically. This is done by characterising (by a formula) states in which an event may cause interaction. The existence of such states does not automatically imply that there is feature interaction: these states might not be reachable. We therefore describe a method and tool which attempts to decide whether a state that satisfies the formula is reachable. (We say 'attempts' because this problem is undecidable in general.)
Ulrike Peiker, Martin Griebl