X hits on this document

Powerpoint document

Requirements Decomposition Analysis, Model Based Testing of Sequential Code Properties - page 14 / 17

35 views

0 shares

0 downloads

0 comments

14 / 17

20 July, 2004

OSMA Software Assurance Symposium

14

California Institute of Technology

Model Based Testing of Sequential Code Properties Highlights (cont’d)

Accuracy

Lurch confirmed deadlock violations found earlier with SPIN

Lurch provided easier access (than SPIN) to information about the location of C code faults

After faults repaired

The new C code is used in conjunction with the old SPIN model

The number of SPIN reported verification problems was reduced by half

SPIN subsequently ran out of memory before quitting

RA-RRE Model still too big for LURCH

Document info
Document views35
Page views35
Page last viewedMon Dec 05 17:13:30 UTC 2016
Pages17
Paragraphs299
Words1977

Comments