Inspiring Applications of SpinFlood Control 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. |
|
|
|
Call Processing 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 Mars Science Laboratory, Deep Space 1, Cassini, the Mars Exploration Rovers, Deep Impact, etc. A description of the work done on MSL can be found here. 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 (pdf). 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 report, and the more detailed appendix). 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. |
|