The Feature Constuct in Programming and Specification Languages

An EPSRC research project

Mark Ryan and Marta Kwiatkowska

The project concerns the ``feature interaction problem'' in software systems. A feature is a unit of functionality that may be added to (or omitted from) a system. Examples of features are plug-ins for software packages or additional services offered by telecommunications providers. The feature interaction problem arises when several features co-exist in a system, and may interfere with each other in ways which are undesirable and hard to predict.

The project uses model checking to verify the absence (or presence) of feature interactions. `Model checkers' are software tools which enable automatic checking of systems against specifications: when supplied with a description of a system and the intended specification they output `yes' if the specification is satisfied, and `no' otherwise. In the latter case, a counter-example (a trace leading to error) is output as well. Model checking, and particularly symbolic model checking, has become an established tool for use in ensuring correctness of systems as well as exposing flaws in the existing designs, and is rapidly becoming an industry standard in hardware verification (see e.g. tools SMV, Spin, Mocha, FDR).

The main obstacle in using model checking is the state explosion problem: the fact that the number of possible states of a system is exponential in the size of the system (as measured, for example, by its number of components or variables). Successful use of model checking involes employing state-of-the-art techniques to address the state explosion problem, such as:

• abstraction: given a system to be model-checked against a specification, it may be possible to determine that some aspects of the system are irrelevant to the specification and can be abstracted.
• decomposition: it may be possible to decompose the system into smaller subsystems, to model check these independently, and to put the results together to form a conclusion about the global system.
• symmetry reduction: a system which is composed of n identical parts (which is the case for telecommunication systems) exhibits symmetries which it may be possible to exploit.

The project involves both the development of such techniques, and the application and deployment of them in featured systems. Another dimension of the project concerns the trade-off between expressive power and efficiency in model checking. Temporal logics such as LTL, CTL, and ATL (`Alternating-time Temporal Logic') and languages such as CSP and CCS differ in their expressive power and have associated with them model-checking tools employing different algorithms, yielding a variety of systems. The requirements imposed by the feature interaction problem and the telecomunications domain need to be precisely understood in order to choose between the available techniques.

The project involves both theoretical work and practical implementation and case-study development.

Research Fellow

Dr. Dimitar Guelev has been appointed as research fellow on this project.

Last modified: 1 January 2002.