Theorem proving for product line model verification

被引：0

作者：

Mannion, M ^{[1
]}

Camara, J ^{[1
]}

机构：

[1] Glasgow Caledonian Univ, Sch Comp & Math Sci, Glasgow G4 0BA, Lanark, Scotland

来源：

SOFTWARE PRODUCT-FAMILY ENGINEERING | 2004年 / 3014卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Product line models of requirements can be used to drive the selection of requirements of new systems in the product line. Validating any selected single system is difficult because product line models are large and complex. However by modelling variability and dependency between requirements using propositional connectives a logical expression can be developed for the model and then selection validation can be achieved by satisfying the logical expression. This approach can be used to validate the model as a whole. A case study with nearly 800 requirements is presented and the computational aspects of the approach are discussed.

引用

下载

页码：211 / 224

页数：14

共 50 条

[1] Theorem proving for verification
Harrison, John
COMPUTER AIDED VERIFICATION, 2008, 5123 : 11 - 18
[2] Divider circuit verification with model checking and theorem proving
Kaivola, R
Aagaard, MD
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 338 - 355
[3] Theorem proving languages for verification
Jouannaud, JP
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2004, 3299 : 11 - 14
[4] A lightweight integration of theorem proving and model checking for system verification
Kong, WQ
Ogata, K
Seino, T
Futatsugi, K
12th Asia-Pacific Software Engineering Conference, Proceedings, 2005, : 59 - 66
[5] Verification of AMBA Using a Combination of Model Checking and Theorem Proving
Amjad, Hasan
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 145 : 45 - 61
[6] Accurate theorem proving for program verification
Cook, Byron
Kroening, Daniel
Sharygina, Natasha
LEVERAGING APPLICATIONS OF FORMAL METHODS, 2006, 4313 : 96 - 114
[7] Theorem Proving for Verification: The Early Days
Moore, J. Strother
25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, : 283 - 283
[8] Interactive Theorem Proving and Verification FOREWORD
Natarajan, Raja
SADHANA-ACADEMY PROCEEDINGS IN ENGINEERING SCIENCES, 2009, 34 (01): : 1 - 2
[9] Hybrid verification integrating HOL theorem proving with MDG model checking
Mizouni, Rabeb
Tahar, Sofiene
Curzon, Paul
MICROELECTRONICS JOURNAL, 2006, 37 (11) : 1200 - 1207
[10] Verification condition generation via theorem proving
Matthews, John
Moore, J. Strother
Ray, Sandip
Vroon, Daron
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2006, 4246 : 362 - 376

← 1 2 3 4 5 →