Model-checking the preservation of temporal properties upon feature integration

Dimitar P. Guelev, Mark Ryan, Pierre Yves Schobbens

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

Abstract

Model checking is a popular technique for proving properties of systems. When systems are updated with new features, however, one would like to avoid having to re-run the model checking procedure on properties which were true before the update, in order to check that they are still true afterwards. This paper proposes a technique which, in certain circumstances, enables such additional checks to be avoided.

Original languageEnglish
Title of host publicationProceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004)
Pages311-324
Number of pages14
Volume128
Edition6
DOIs
Publication statusPublished - 23 May 2005
EventProceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004) -
Duration: 4 Sep 20044 Sep 2004

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
ISSN (Print)1571-0661

Conference

ConferenceProceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004)
Period4/09/044/09/04

Keywords

  • Features
  • Model checking
  • Property preservation
  • Safety properties
  • Temporal properties

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

Cite this