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 条

[31] Towards Flight Control Verification Using Automated Theorem Proving
Denman, William
Zaki, Mohamed H.
Tahar, Sofiene
Rodrigues, Luis
NASA FORMAL METHODS, 2011, 6617 : 89 - 100
[32] A dynamic logic for verification of synchronous models based on theorem proving
Yuanrui ZHANG
Frdric MALLET
Zhiming LIU
Frontiers of Computer Science, 2022, 16 (04) : 228 - 230
[33] A theorem proving framework for the formal verification of Web Services Composition
Papapanagiotou, Petros
Fleuriot, Jacques D.
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (61): : 1 - 16
[34] A dynamic logic for verification of synchronous models based on theorem proving
Yuanrui Zhang
Frédéric Mallet
Zhiming Liu
Frontiers of Computer Science, 2022, 16
[35] EFFICIENT RT-LEVEL VERIFICATION BY THEOREM-PROVING
MARGARIA, T
IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1992, 12 : 696 - 702
[36] An approach for the formal verification of DSP designs using theorem proving
Akbarpour, Behzad
Tahar, Sofiene
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2006, 25 (08) : 1441 - 1457
[37] HVoC: a Hybrid Model Checking-Interactive Theorem Proving Approach for Functional Verification of Digital Circuits
Minhas, Mishal Fatima
Hasan, Osman
Abed, Sa'ed
JOURNAL OF ELECTRONIC TESTING-THEORY AND APPLICATIONS, 2021, 37 (04): : 561 - 567
[38] Relational STE and Theorem Proving for Formal Verification of Industrial Circuit Designs
O'Leary, John
Kaivola, Roope
Melham, Tom
2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2013, : 97 - 104
[39] FORMAL VERIFICATION OF FAULT TOLERANCE USING THEOREM-PROVING TECHNIQUES
KLJAICH, J
SMITH, BT
WOJCIK, AS
IEEE TRANSACTIONS ON COMPUTERS, 1989, 38 (03) : 366 - 376
[40] General purpose theorem proving methods in the verification of digital hardware and software
Moore, JS
VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 14 - 35

← 1 2 3 4 5 →