X hits on this document

Powerpoint document

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

37 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 views37
Page views37
Page last viewedWed Dec 07 20:21:11 UTC 2016
Pages17
Paragraphs299
Words1977

Comments