| 
|
Quote: SPIN found five errors in part of the LISP code for NASA's Remote Agent; took 12 man weeks to model and one week to verify
Topic:
limitations of formalism
Topic:
model checker
Quotation Skeleton
The effort consisted of hand translating parts of … verifying two properties formulated by the Remote Agent … Both properties turned out to be broken, and … [p. 763] The modeling effort, obtaining a PROMELA program … … [took] about one week. The model checker found … Google-1 Google-2
Copyright clearance needed for quotation.
Topic: limitations of formalism (93 items)
Topic: model checker (49 items)