[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Klaus Havelundd & Mike Lowry & John Penix
- Formal analysis of a Space-Craft Controller using SPIN
- IEEE Trans Software Engineering V27n8(Aug 2001)pp749-765
- =CASESTUDY FORMAL MODEL CHECKING TOOL SPIN LISP LTLMODAL LOGIC ESL PROMELA
- Deep Space 1.
- Located a major design flaw.
- found a bug that testing missed that caused problem 98M kilometers from Earth.
- LTL::="Linear Temporal Logic", properties of traces using modes  = always and <> meaning some.
- 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 for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]