Incremental specification of telecommunication services

This paper presents the specification of telecommunication services using B abstract machines, and it defines the feature interaction problem as an interference issue among processes sharing common resources. The work reported is experimental in nature as we explore the way in which to use the B method to tackle the feature interaction problem in telecommunication services. The B method is a tool for specifying, refining and developing systems in a mathematical and rigorous, but simple, way. Services are specified using the B method and the feature interaction problem is modelled as a violation of invariant properties. The B method is supported by software that helps the specifier of services and features. We have not only modelled services within the B technology, but we have also extended the B methodology with a novel way of combining abstract machines.