Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
Pages: 1
#1 2014-02-02 00:12:03
Application of Spin to the Mars Curiosity Rover
See the February issue of the Communications of the ACM
with an article 'Mars Code' describing how the JPL Flight Software
Team extracted Spin models directly from implementation
level C code to perform logic model checking.
http://cacm.acm.org/magazines/2014/2/171689-mars-code/fulltext
The Rover code is notably more robust than that of earlier
missions to Mars, even though the MSL spacecraft used
more code than all previous missions to Mars combined.
Offline
Pages: 1