A Research Project with BT

Mark Ryan
School of Computer Science
University of Birmingham
Edgbaston
Birmingham B15 2TT
Tel +44 121 414 7361
Fax +44 121 414 4281
Email mdr@cs.bham.ac.uk

August 1996

Executive Summary

Main objective.

This project will address the problem of adding features to specifications of complex software products, in particular software for telecommunication services.

Why is this important?

Complex software systems nearly always have an extended lifetime during which requirements change, e.g. because users become more sophisticated or because the underlying technology supports more capabilities. Meeting new requirements may involve changing existing components or adding new components. The more complex the system is the harder it is to make such changes without breaking something; this problem has been dubbed the `feature interaction problem'. Methods and tools to overcome these problems are potentially of immense commercial value to BT.

How will it be done?

This project will provide tools and a methodology to overcome these difficulties. This has two main strands: providing a new means of specifying complex systems and their functions precisely, and providing new tools for manipulating the specifications.

In particular, the project will deliver:

• a feature-oriented specification language, based on an existing specification language, optimised for specifying featured communication services. The language will be used to model features and to prove properties about their interactions.
• Verification methods and tools for detecting and explaining conflicts between features; deducing consequences of feature combinations; and constructing test suites for feature combinations, and providing typical scenarios.

This will extend and apply theoretical ideas already developed by the author. In order to test the language and tools and help to explain the methodology to potential users, the project will also deliver:

• Several case studies assessing the adequacy of the language and tools. The case studies will be chosen from services relevant to BT's business, such as: telephone services, mobile communications, multi-media, video conferencing.

Technical discussion

Telecommunication companies face considerable problems when they introduce, remove, or re-specify services. BT is aware of this, as evidenced by its group on feature interactions, led by Mel Bale. Two important such problems are:

• The specification of any particular service is widely distributed over the specification of the whole system. This means that it is difficult to gain conceptual understanding of the requirements and effects of service. It is also hard to remove the service, or to take the service and introduce it into a different system. In short, it is not possible to treat the service as a single unit.

• Services may interact together in ways that are hard to predict; indeed, the introduction of a service can prevent the correct working of one previously introduced. This is known as the `feature interaction problem', and has emerged as a major topic in software engineering [,]. Quite a lot is known about different types of feature interactions, but the problem of detecting and resolving them is unsolved.

The provision of a service is a feature of the telecommunications system, and hence one can loosely use the terms `service' and `feature' interchangeably. (Strictly speaking, a service might imply several distinct features, and also there might be features which don't correspond to any service.)

Current trends in telecommunications indicate that software development methods will have to give much better support for the easy introduction of new services. This requires a paradigm shift towards feature-orientation, away from the purely resource-oriented nature of (for example) current object-oriented methods.

This project proposes the feature as a structuring mechanism for specifications. It will deliver a feature-oriented specification language, in which the specification of a feature or service is a self-contained, compact unit which can be introduced in any specification that satisfies certain minimal requirements determined by the service. This will address the first of the two problems mentioned.

The specification language will be supported by a logic which can be used to prove properties about specifications. This will enable feature interactions to be described and analysed. This will address the second problem.

The design of the specification language will start from the classical object-oriented (OO) structuring mechanism. Indeed, recent experience in the OO community in formal requirements specification also points to the need for a higher-level module notion than the object description. The expectations raised by object-orientation concerning the ease of adapting existing systems to new requirements have not been fulfilled. The inheritance mechanism has been shown to be insufficient. A larger-scale mechanism allowing consistent, simultaneous introduction of new and specialised classes is required.

Until recently it was not clear how to set up such a mechanism although several proposals have appeared in the literature. The goal of the project relies on bringing together these two views (the feature view emerging in telecommunications, and the need for a high-level structuring mechanism in OO) by recognising that the needed structuring concept should be identified with the feature.

The technical proposal

The proposal is to define a specification language and logic in which features are first-class objects. That means that the feature is a basic structuring mechanism. The language will allow features to be added, removed, or respecified with relative ease, and will allow features designed for one specification to be applied to another (provided certain conditions which form part of the feature are met). It will provide a language for checking feature interactions and resolving them.

Work activities

1. The appointed PhD student will spend approximately two weeks at BT Labs, learning about telecommunication services and BT's research work.

2. Identification of temporal and kernel languages. The Project will identify a suitable temporal logic specification language which will be used as the starting point for the feature-oriented language. This `temporal language' should
   • be object-oriented, with built-in locality handling, and
   • have implicit the notion of state, since telephony examples are state-based.
   Candidates for the temporal language include Lamport's TLA [], Pnueli's LTL [], SMV [,], and others. The project will also work with a small `kernel language' (first-order logic) which will enable features to be studied abstractly, avoiding early commitments in the final user language.

3. Feature extension. For the temporal language and the kernel language, devise a suitable syntax and semantics for the `feature' construct. The syntax will identify in a suitably general way the components which are required of the specification in order for the feature to be applied, and the result of the application. The semantics will be based on parameterised specifications and defaults.

4. Verification tools and methods. A single PhD student on a three year project will not be able to write a comprehensive set of tools from scratch. However, the candidate temporal languages were chosen partly because they already have tools. We will modify these and/or use them in conjunction with a preprocessor for dealing with the feature constructs.

   Model-checking is emerging as a powerful verification technique which is attracting industrial attention because of its ability to deal with large-scale verification problems. The SMV language described above is specifically designed for model-checking, but other languages can also benefit from model-checking technology, if a method for generating canonical transition systems from specifications can be found. This is a new and exciting approach to automatic verification of temporal properties which is not expected to suffer from the intractabilities of traditional theorem proving.

5. Feature interactions. Logic-based techniques will be investigated for detecting unwanted feature interactions, and for pinpointing the specification parts involved. The classifications of interactions in [] and [] will be revised, adopting a logic point of view.

   The main tool produced will be a query evaluator, which will be able to evaluate whether a given featured specification has certain properties or not. This will be able to deal with some types of interaction, such as deadlock. Later, it will be extended for other types of interaction. When the system fails to satisfy the property, the technique will generate a typical example of the interaction (using, eg, model checking and tableaux approaches).

6. Case studies. Some case studies will motivate the feature construct and provide a benchmark for assessing its adequacy. It is expected that BT will provide many case studies, such as those arising from its video-on-demand experiment in Ipswich and Colchester (which allows concurrent telephone calls). Other possibilities for case studies include:
   • POTS with some well-known features (CFU, ACBS, VMB,...).
   • Mobile telephone and network features.
   • Multimedia services, such as those provided by cable TV companies, video conferencing, and distance learning.
   • Multi-capability person-to-person communication technologies, integrating telephone, email, fax.
   • World wide web -- although currently most interactive WWW pages are based on ad-hoc programming via CGI, tools such as HotJava are emerging for providing standard services and features, with attendant interactions.

7. Test data selection. Techniques for generating test data will be developed. This will use standard techniques, noting that the structuring mechanism of a feature-oriented approach allows better focussing of the test effort than a purely object oriented approach, in a similar manner as the modular approach has been a great advance for incremental software validation and verification. These data can be used to test the final implementation, and also provide concrete cases for the end users to validate their intuitions about the informal specification.

There will be considerable overlap between these tasks, but broadly speaking, items (1)-(3) and some of the case studies are intended to be finished by the first year. During the first year also, the remaining items will be further specified, and carried out in the second and third years.