Model-checking the preservation of temporal properties upon feature integration

Dimitar P. Guelev; Mark Ryan; Pierre Yves Schobbens

doi:10.1016/j.entcs.2005.04.019

Model-checking the preservation of temporal properties upon feature integration

Dimitar P. Guelev, Mark Ryan, Pierre Yves Schobbens

Universite de Namur

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférence › Article dans les actes d'une conférence/un colloque

Résumé

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.

langue originale	Anglais
titre	Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004)
Pages	311-324
Nombre de pages	14
Volume	128
Edition	6
Les DOIs	https://doi.org/10.1016/j.entcs.2005.04.019
Etat de la publication	Publié - 23 mai 2005
Evénement	Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004) - Durée: 4 sept. 2004 → 4 sept. 2004

Série de publications

Nom	Electronic Notes in Theoretical Computer Science
Editeur	Elsevier
ISSN (imprimé)	1571-0661

Une conférence

Une conférence	Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004)
période	4/09/04 → 4/09/04

Accès au document

10.1016/j.entcs.2005.04.019

Autres fichiers et liens

Link to publication in Scopus

Contient cette citation

@inproceedings{2d4c69c642574ddfba9e0ed3a984611a,

title = "Model-checking the preservation of temporal properties upon feature integration",

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.",

keywords = "Features, Model checking, Property preservation, Safety properties, Temporal properties",

author = "Guelev, {Dimitar P.} and Mark Ryan and Schobbens, {Pierre Yves}",

year = "2005",

month = may,

day = "23",

doi = "10.1016/j.entcs.2005.04.019",

language = "English",

volume = "128",

series = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier",

pages = "311--324",

booktitle = "Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004)",

edition = "6",

note = "Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004) ; Conference date: 04-09-2004 Through 04-09-2004",

}

Guelev, DP, Ryan, M & Schobbens, PY 2005, Model-checking the preservation of temporal properties upon feature integration. Dans Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004). 6 edn, VOL. 128, Electronic Notes in Theoretical Computer Science, p. 311-324, Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004), 4/09/04. https://doi.org/10.1016/j.entcs.2005.04.019

Model-checking the preservation of temporal properties upon feature integration. / Guelev, Dimitar P.; Ryan, Mark; Schobbens, Pierre Yves.
Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004). Vol 128 6. Ed. 2005. p. 311-324 (Electronic Notes in Theoretical Computer Science).

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférence › Article dans les actes d'une conférence/un colloque

TY - GEN

T1 - Model-checking the preservation of temporal properties upon feature integration

AU - Guelev, Dimitar P.

AU - Ryan, Mark

AU - Schobbens, Pierre Yves

PY - 2005/5/23

Y1 - 2005/5/23

N2 - 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.

AB - 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.

KW - Features

KW - Model checking

KW - Property preservation

KW - Safety properties

KW - Temporal properties

UR - http://www.scopus.com/inward/record.url?scp=18744397522&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2005.04.019

DO - 10.1016/j.entcs.2005.04.019

M3 - Conference contribution

AN - SCOPUS:18744397522

VL - 128

T3 - Electronic Notes in Theoretical Computer Science

SP - 311

EP - 324

BT - Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004)

T2 - Proceedings of the Fouth International Workshop on Automate Verification of Critical Systems (AVoCS 2004)

Y2 - 4 September 2004 through 4 September 2004

ER -

Model-checking the preservation of temporal properties upon feature integration

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation