Model-checking the preservation of temporal properties upon feature integration

Updating a system by adding new features to it is a technique which enables designs and code to be reused. However, adding new features can remove some properties of the system, as well as adding other ones. Model checking can be used to check whether important properties have been lost when a feature was added, but, as is well-known, model checking is computationally expensive. In this paper, we develop a method which avoids the necessity to re-check certain properties of systems when a feature is added. The method provides criteria allowing us to deduce that the feature does not break a given property, and it is computationally simpler to check the criteria than to perform the model checking. The method is sound, but in general it is not complete: it may not be able to conclude that a property holds of a featured system even if it does hold. In the case of safety properties, we give an intuitive explanation of why it is likely to be complete in practice.