Model-checking the preservation of temporal properties upon feature integration

Dimitar P. Guelev, Mark D. Ryan, Pierre Yves Schobbens

Résultats de recherche: Contribution à un journal/une revueArticleRevue par des pairs


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.

langue originaleAnglais
Pages (de - à)53-62
Nombre de pages10
journalInternational Journal on Software Tools for Technology Transfer
Numéro de publication1
Les DOIs
Etat de la publicationPublié - 1 févr. 2007

Empreinte digitale

Examiner les sujets de recherche de « Model-checking the preservation of temporal properties upon feature integration ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation