Theoretical foundations of updating systems

Software systems inevitably require update and revision during their lifetime. The concept of features is often used to model system update: a feature is a unit of functionality which may be integrated into a base system. Possible features of an email client program include: spam filtering; absence messages; selective forwarding; and encryption. In our work, we use AI techniques to understand the operation of feature integration more clearly. In particular, we have taken SMV (symbolic model verifier) feature integrator (SFI), a tool which automates feature integration on systems described using the model checker SMV. Then we have taken update which is an operation of theory change, closely related to belief revision, and defined over propositional logic. We formulate and prove a theorem stating that SFI feature integration is an update operation.