TY - JOUR
T1 - Model-checking the preservation of temporal properties upon feature integration
AU - Guelev, Dimitar P.
AU - Ryan, Mark D.
AU - Schobbens, Pierre Yves
PY - 2007/2/1
Y1 - 2007/2/1
N2 - 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.
AB - 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.
KW - Feature
KW - Model checking
KW - Property preservation
KW - State-explosion problem
UR - http://www.scopus.com/inward/record.url?scp=33947598081&partnerID=8YFLogxK
U2 - 10.1007/s10009-006-0006-x
DO - 10.1007/s10009-006-0006-x
M3 - Article
AN - SCOPUS:33947598081
SN - 1433-2779
VL - 9
SP - 53
EP - 62
JO - International Journal on Software Tools for Technology Transfer
JF - International Journal on Software Tools for Technology Transfer
IS - 1
ER -