X hits on this document

Powerpoint document

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

57 views

0 shares

0 downloads

0 comments

5 / 17

20 July, 2004

OSMA Software Assurance Symposium

5

California Institute of Technology

Requirements Decomposition Analysis Goals and Objectives (cont’d)

Model Based Testing of Sequential Code Properties

1.

Goal: Determine whether reduced-state model checking can be as effective as traditional model checking

2.

Objectives:

Manually translate an existing formal model of a JPL system into LURCH

MER Arbiter

Apply LURCH and traditional model checking techniques (i.e., SPIN) to the models

Compare the effectiveness of LURCH and SPIN in identifying errors in the models.

Document info
Document views57
Page views57
Page last viewedMon Jan 23 05:24:37 UTC 2017
Pages17
Paragraphs299
Words1977

Comments