Model-checking the preservation of temporal properties upon feature integration

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

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish
Pages (from-to)53-62
Number of pages10
JournalInternational Journal on Software Tools for Technology Transfer
Issue number1
Publication statusPublished - 1 Feb 2007


  • Feature
  • Model checking
  • Property preservation
  • State-explosion problem


Dive into the research topics of 'Model-checking the preservation of temporal properties upon feature integration'. Together they form a unique fingerprint.

Cite this