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

共 12 条

[1] Amyot D., 2003, FEATURE INTERACTIONS
[2] Armoni R, 2002, LECT NOTES COMPUT SC, V2280, P296
[3] BOUMA L, 1992, P 1 INT WORKSH FEAT
[4] Calder M., 2001, Model Checking Software. 8th International SPIN Workshop. Proceedings (Lecture Notes in Computer Science Vol.2057), P143
[5] Calder M., 2000, FEATURE INTERACTIONS
[6] du Bousquet L, 1999, LECT NOTES COMPUT SC, V1708, P622
[7] HALPERN J, 1983, LECT NOTES COMPUT SC, V154, P278
[8] Huth M, 2000, LOGIC COMPUTER SCI M
[9] Temporal logic with forgettable past
Laroussinie, F
Markey, N
Schnoebelen, P
[J]. 17TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2002, : 383 - 392
[10] Lichtenstein O., 1985, Logics of Programs. Proceedings, P196

← 1 2 →