Model-checking the Preservation of Temporal Properties upon Feature Integration

被引：2

作者：

Guelev, Dimitar P. ^{[1
]}

Ryan, Mark ^{[1
]}

Schobbens, Pierre Yves ^{[2
]}

机构：

[1] Univ Birmingham, Sch Comp Sci, Birmingham, W Midlands, England

[2] Fac Univ Namur, Inst Informat, Namur, Belgium

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2005年 / 128卷 / 06期

关键词：

Model checking; features; temporal properties; safety properties; property preservation;

D O I：

10.1016/j.entcs.2005.04.019

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：311 / 324

页数：14

共 50 条

[1] Model-checking the preservation of temporal properties upon feature integration
Guelev D.P.
Ryan M.D.
Schobbens P.Y.
[J]. International Journal on Software Tools for Technology Transfer, 2007, 9 (1) : 53 - 62
[2] TAGED Approximations for Temporal Properties Model-Checking
Courbis, Romeo
Heam, Pierre-Cyrille
Kouchnarenko, Olga
[J]. IMPLEMENTATION AND APPLICATION OF AUTOMATA, PROCEEDINGS, 2009, 5642 : 135 - 144
[3] Model-checking Timed Temporal Logics
Bouyer, Patricia
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 323 - 341
[4] Model-checking temporal behaviour in CSP
Ouaknine, J
Reed, GM
[J]. INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, PROCEEDINGS, 1999, : 295 - 304
[5] Model-Checking Temporal Properties of Real-Time HTL Programs
Carvalho, Andre
Carvalho, Joel
Pinto, Jorge Sousa
de Sousa, Simao Melo
[J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT II, 2010, 6416 : 191 - +
[6] From Model-Checking to Temporal Logic Constraint Solving
Fages, Francois
Rizk, Aurelien
[J]. PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING, 2009, 5732 : 319 - 334
[7] On the Decidability of Model-Checking Information Flow Properties
D'Souza, Deepak
Holla, Raveendra
Kulkarni, Janardhan
Ramesh, Raghavendra K.
Sprick, Barbara
[J]. INFORMATION SYSTEMS SECURITY, PROCEEDINGS, 2008, 5352 : 26 - +
[8] Model-checking data-aware temporal workflow properties with CTL-FO+
Halle, Sylvain
Villemaire, Roger
Cherkaoui, Omar
Ghandour, Boubker
[J]. 11TH IEEE INTERNATIONAL ENTERPRISE DISTRIBUTED OBJECT COMPUTING CONFERENCE, PROCEEDINGS, 2007, : 267 - 278
[9] The model-checking kit
Schröter, C
Schwoon, S
Esparza, J
[J]. APPLICATIONS AND THEORY OF PETRI NETS 2003, PROCEEDINGS, 2003, 2679 : 463 - 472
[10] Integration of model-checking tools: from Discrete to hybrid models
Mufti, Waseem A.
Tcherukine, Dimitri C.
[J]. INMIC 2007: PROCEEDINGS OF THE 11TH IEEE INTERNATIONAL MULTITOPIC CONFERENCE, 2007, : 106 - 109

← 1 2 3 4 5 →