Formal verification coverage: computing the coverage gap between temporal specifications

被引：8

作者：

Das, S ^{[1
]}

Basu, P ^{[1
]}

Banerjee, A ^{[1
]}

Dasgupta, P ^{[1
]}

Chakrabarti, PP ^{[1
]}

Mohan, CR ^{[1
]}

Fix, L ^{[1
]}

Armoni, R ^{[1
]}

机构：

[1] Indian Inst Technol, Dept Comp Sci & Engn, Kharagpur, W Bengal, India

来源：

ICCAD-2004: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, IEEE/ACM DIGEST OF TECHNICAL PAPERS | 2004年

关键词：

D O I：

10.1109/ICCAD.2004.1382571

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Existing methods for formal verification coverage compare a given specification with a given implementation, and evaluate the coverage gap in terms of quantitative metrics. In this paper, we consider a new problem, namely to compare two formal temporal specifications and to find a set of additional temporal properties that close the coverage gap between the two specifications. In this paper we present: (1) the problem definition and motivation, (2) a methodology for computing the coverage gap between specifications, and (3) a methodology for representing the coverage gap as a collection of temporal properties that preserve the syntactic structure Of the target specification.

引用

页码：198 / 203

页数：6

共 50 条

[31] Bridging the Gap between testing and formal verification in Ada Development
Marche, Claude
Kanig, Johannes
ERCIM NEWS, 2015, (100): : 38 - 39
[32] Parallel computing of radio coverage
Kuonen, P
Josselin, S
Ubeda, S
Wagner, D
1996 IEEE 46TH VEHICULAR TECHNOLOGY CONFERENCE, PROCEEDINGS, VOLS 1-3: MOBILE TECHNOLOGY FOR THE HUMAN RACE, 1996, : 1438 - 1442
[33] FACTORS FOR COMPUTING PHOTO COVERAGE
LUND, HG
PHOTOGRAMMETRIC ENGINEERING, 1969, 35 (01): : 61 - &
[34] Gap between the US and Japan in coverage of pharmacogenomic biomarkers by health insurance programs: More coverage is needed in Japan
Hikino, Keiko
Fukunaga, Koya
Mushiroda, Taisei
DRUG METABOLISM AND PHARMACOKINETICS, 2018, 33 (06) : 243 - 249
[35] Bridging the Gap Between Requirements Document and Formal Specifications using Development Patterns
Sayar, Imen
Souquieres, Jeanine
2019 IEEE 27TH INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE WORKSHOPS (REW 2019), 2019, : 116 - 122
[36] Bridging the Gap Between Informal Requirements and Formal Specifications Using Model Federation
Golra, Fahad Rafique
Dagnat, Fabien
Souquieres, Jeanine
Sayar, Imen
Guerin, Sylvain
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2018, 2018, 10886 : 54 - 69
[37] POWER-TRUCTOR: An Integrated Tool Flow for Formal Verification and Coverage of Architectural Power Intent
Hazra, Aritra
Mukherjee, Rajdeep
Dasgupta, Pallab
Pal, Ajit
Harer, Kevin M.
Banerjee, Ansuman
Mukherjee, Subhankar
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2013, 32 (11) : 1801 - 1813
[38] Early formal verification of conditional coverage points to identify intrinsically hard-to-verify logic
Ho, C. Richard
Theobald, Michael
Deneroff, Martin M.
Dror, Ron O.
Gagliardo, Joseph
Shaw, David E.
2008 45TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2008, : 268 - 271
[39] Cryptographic verification of test coverage claims
Devanbu, PT
Stubblebine, SG
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2000, 26 (02) : 178 - 192
[40] Coverage centralities for temporal networks
Taro Takaguchi
Yosuke Yano
Yuichi Yoshida
The European Physical Journal B, 2016, 89

← 1 2 3 4 5 →