Feature interaction detection: a LOTOS-based approach
A methodology to detect feature interactions in the design of telephone systems is presented. First, the system with its features is specified in language of temporal ordering specification (LOTOS). With the use of tools, the specification is then expanded into a state transition model, representing either the entire global state space or significant portions of it. Properties describe proper system and feature behavior; violations to these properties are symptoms of feature interaction. Observers, watchdogs, and trace analysis tools are constructed to check for deviations from these properties. These processes are used to search the state transitions, both during and after the construction of the state transition model. Traces presenting violation of properties are printed as message sequence charts (MSCs).
feature interaction detection lotos telephony systems formal techniques formal validation