A framework for computer-aided validation

被引:7
作者
Drusinsky, Doron [1 ]
Michael, James Bret [1 ]
Shing, Man-Tak [1 ]
机构
[1] US Navy, Postgrad Sch, Dept Comp Sci, 1411 Cunningham Rd, Monterey, CA 93943 USA
基金
美国国家航空航天局;
关键词
Validation and verification; Formal methods; Model checking; Runtime verification;
D O I
10.1007/s11334-008-0047-2
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper presents a framework for augmenting independent validation and verification (IV&V) of software systems with computer-based IV&V techniques. The framework allows an IV&V team to capture its own understanding of the application as well as the expected behavior of any proposed system for solving the underlying problem by using an executable system reference model, which uses formal assertions to specify mission- and safety-critical behaviors. The framework uses execution-based model checking to validate the correctness of the assertions and to verify the correctness and adequacy of the system under test.
引用
收藏
页码:161 / 168
页数:8
相关论文
共 9 条
[1]   Misuse cases: Use cases with hostile intent [J].
Alexander, I .
IEEE SOFTWARE, 2003, 20 (01) :58-+
[2]  
[Anonymous], 1998, 12331998 IEEE, DOI [10.1109/IEEESTD.1998.88826, DOI 10.1109/IEEESTD.1998.88826]
[3]  
Drusinsky D, 2006, MODELING VERIFICATIO
[4]  
Drusinsky D, 2007, IEEE DISTRIBUTED SYS, V8
[5]  
Drusinsky D, 2007, OVERVIEW ROUTING PRO
[6]  
Havelund K., 2000, STTT, V2, P366
[7]  
Heitmeyer CL, 2007, J UNIVERS COMPUT SCI, V13, P607
[8]  
*IEEE, 2004, 10122004 IEEE
[9]  
IEEE, 1990, 610121990 IEEE