Feature Integration as Substitution 
Dimitar P. GUELEV, Mark D. RYAN and Pierre Yves SCHOBBENS
School of Computer Science, Birmingham University, UK
E-mail: {D.P.Guelev, M.D.Ryan}@cs.bham.ac.uk
Institut d’Informatique, Facultés Universitaires de Namur, Belgium
E-mail: pys@info.fundp.ac.be
Abstract. In this paper we analyse the development of automated systems
by means of adding features to a basic system. Our approach is to describe
systems in temporal logic. We regard the process of integrating features as
a transformation of those temporal logic descriptions. We use substitution
of predicates as the basic means to achieve feature readiness of descriptions
and define feature integration.We show that several description formalisms
for features known from the literature can be fitted into the formal framework
of our analysis, despite the fact that they have been initially motivated
by different observations. Among these formalisms are Samborski’s stack service
model, the feature construct for SMV and others. We argue that the way to
address the verification problems which are specific to systems with features
provided by our analysis is clear, convenient and based on classical and well
established logical notions only. The logic we use in examples of description
in this paper is the duration calculus with higher order quantifiers and iteration.