Three examples of inspiring applications of Spin in the last few years include
the verification of the control algorithms for the new flood control
barrier built in the late nineties near Rotterdam in the Netherlands.
The verification work was carried out by the Dutch firm CMG
(Computer Management Group) in collaboration with the Formal Methods
group at the University of Twente.
Logic verification of the call processing software for a commercial data
and phone switch, the PathStar switch that was designed and built at
Lucent Technologies. The application was based on model
extraction from the full and unmodified ANSI-C code of the implementation,
which was checked for compliance with a group of roughly 20 class-5 features
formalized in linear temporal logic (e.g., call waiting, conference calling, etc.).
A cluster of 16 CPUs was used to perform the verifications overnight, every day
for a period of several months before the switch was marketed.
Perhaps the largest application of software model checking to date.
Mission Critical Software
Selected algorithms for a number of space missions were verified with
the Spin model checker. The missions include Deep Space 1, Cassini,
the Mars Exploration Rovers, Deep Impact, etc.
For Cassini, we verified the correct working of the handoff algorithms
for the dual control CPUs (pdf).
For Deep Space 1, researchers at Ames Research Center verified some
key algorithms and reported their findings in a technical report
(pdf1 which appeared in
IEEE Transactions on Software Engineering, Volume 27, Number 8, August 2001,
and the post-mortem analysis in pdf2
which appeared at the Fifth NASA Langley Formal Methods Workshop, Virginia, June 2000).
Later, at JPL a separate verification of the software used on this mission
was also done (pdf).
For the Mars Exploration Rovers we verified the correct working of
the resource arbiter that manages the use of all motors on the rovers
More recently, for Deep Impact we verified aspects of the flash file system module
that had shown problems before the encounter with the comet took place.
The picture to the right shows the Cassini spacecraft. A rapidly expanding
domain of application.
The Toyota Investigation
The model checker Spin and its Swarm verification
front-end were used extensively in NASA's detailed investigation
of the control software of the Toyota Camry MY05. The target of the
investigation, at the reques of the NHTSA from the U.S. Department of Transportation,
and executied in collaboration with the NASA Engineering and Safety Center (NESC),
was to see if the cause for unintended acceleration events could be found in software
(see p 150 of the final
and the more detailed
No direct cause for unintended acceleration was identified in this study, though
it could also not be decisively ruled out within the scope of this study.
Several candidate theories, though, were effectively disproven.
Verification of medical device transmission protocols.
Spin was used for about ten years in the verification of international standards that are used worldwide.
This work started with the
IQPS project at Eindhoven University,
and continued at the University of Groningen, both in The Netherlands.
Standards that were influenced by the Spin verification work include
Firewire IEEE 1394.1 (used in many PCs),
and ISO/IEEE 11073-20601
for medical devices.