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.