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 条
  • [21] Formal verification coverage: Are the RTL-properties covering the design's architectural intent?
    Basu, P
    Das, S
    Dasgupta, P
    Chakrabarti, PP
    Mohan, CR
    Fix, L
    DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, VOLS 1 AND 2, PROCEEDINGS, 2004, : 668 - 669
  • [22] Branch Sequence Coverage Criterion for Testing-Based Formal Verification with Symbolic Execution
    Wang, Rong
    Liu, Shaoying
    2019 COMPANION OF THE 19TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS-C 2019), 2019, : 205 - 212
  • [23] Modular formal verification of specifications of concurrent systems
    Gradara, Sara
    Santone, Antonella
    Vaglini, Gigliola
    Villani, Maria Luisa
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2008, 18 (01): : 5 - 28
  • [24] Formal Verification of AADL Specifications in the Topcased Environment
    Berthomieu, Bernard
    Bodeveix, Jean-Paul
    Chaudet, Christelle
    Dal Zilio, Silvano
    Filali, Mamoun
    Vernadat, Francois
    RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE 2009, 2009, 5570 : 207 - +
  • [25] A simulation approach to verification and validation of formal specifications
    Liu, SY
    FIRST INTERNATIONAL SYMPOSIUM ON CYBER WORLDS, PROCEEDINGS, 2002, : 113 - 120
  • [26] Formal Verification of Security Specifications with Common Criteria
    Morimoto, Shoichi
    Shigematsu, Shinjiro
    Goto, Yuichi
    Cheng, Jingde
    APPLIED COMPUTING 2007, VOL 1 AND 2, 2007, : 1506 - +
  • [27] On fault coverage of tests for finite state specifications
    Petrenko, A
    vonBochmann, G
    Yao, M
    COMPUTER NETWORKS AND ISDN SYSTEMS, 1996, 29 (01): : 81 - 106
  • [28] Formal verification of word-level specifications
    Höreth, S
    Drechsler, R
    DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION 1999, PROCEEDINGS, 1999, : 52 - 58
  • [29] Formal verification of abstract system and protocol specifications
    Schneider, Axel
    Bluhm, Thomas
    Renner, Tobias
    Heinkel, Ulrich
    Knaeblein, Joachim
    Zavala, Reynaldo
    30TH ANNUAL IEEE/NASA SOFTWARE ENGINEERING WORKSHOP, PROCEEDINGS, 2006, : 207 - +
  • [30] Verification criterion directed testing for formal specifications
    Zeng, XM
    Tsai, JJP
    Weigert, TJ
    SEKE '96: THE 8TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, PROCEEDINGS, 1996, : 393 - 399
12345