[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

HavelunddLowryPenix01

  1. Klaus Havelundd & Mike Lowry & John Penix
  2. Formal analysis of a Space-Craft Controller using SPIN
  3. IEEE Trans Software Engineering V27n8(Aug 2001)pp749-765
  4. =CASESTUDY FORMAL MODEL CHECKING TOOL SPIN LISP LTLMODAL LOGIC ESL PROMELA
  5. Deep Space 1.
  6. Located a major design flaw.
  7. found a bug that testing missed that caused problem 98M kilometers from Earth.
  8. LTL::="Linear Temporal Logic", properties of traces using modes [] = always and <> meaning some.
  9. Interviewed programmer about impact of work: found difficult mission-killing bugs -- thought formal meant program proving not finding bugs.

Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]