A Visual Tradeoff Space for Formal Verification and Validation Techniques

被引:13
作者
Drusinsky, Doron [1 ]
Michael, James Bret [2 ]
Shing, Man-Tak [1 ]
机构
[1] USN, Dept Comp Sci, Postgrad Sch, Monterey, CA 93943 USA
[2] USN, Dept Comp Sci & Elect & Comp Engn, Postgrad Sch, Monterey, CA 93943 USA
来源
IEEE SYSTEMS JOURNAL | 2008年 / 2卷 / 04期
基金
美国国家航空航天局;
关键词
Assertion checkers; formal methods; model checking; software verification and validation;
D O I
10.1109/JSYST.2008.2009190
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Numerous techniques exist for conducting computer-assisted formal verification and validation. The cost associated with these techniques varies, depending on factors such as ease of use, the effort required to construct correct requirement specifications for complex real-world properties, and the effort associated with instrumentation of the software under test. Likewise, existing techniques differ in their ability to effectively cover the system under test and its associated requirements. To aid software engineers in selecting the appropriate technique for the formal verification or validation task at hand, we introduce a three-dimensional tradeoff space encompassing both cost and coverage.
引用
收藏
页码:513 / 519
页数:7
相关论文
共 52 条
[1]  
[Anonymous], 1981, SCI PROGRAMMING, DOI DOI 10.1007/978-1-4612-5983-1
[2]  
APT KR, 1997, VERIFICATION VALIDAT
[3]   TAME: Using PVS strategies for special-purpose theorem proving [J].
Archer, M .
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2000, 29 (1-4) :139-181
[4]  
Barnes J., 2000, Ada Letters, V20, P69
[5]  
BJORNER NS, 1996, LNCS, V1102, P415
[6]  
BOEHM BW, 1988, COMPUTER, V21, P61, DOI 10.1145/12944.12948
[7]  
BOURQUE P, 2004, SWEBOK GUIDE SOFTWAR
[8]  
BOWEN J, 2006, IEEE COMPUT, V29, P40
[9]  
Boyer R. S., 1988, A Computational Logic Handbook
[10]  
Bozga M, 1998, LECT NOTES COMPUT SC, V1427, P546, DOI 10.1007/BFb0028779