Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
Pages: 1
#1 2014-02-06 06:44:01
CACM article
The February issue of the Communications of the ACM
has an article 'Mars Code' that describesg how the JPL Flight Software
Team extracted Spin models directly from implementation
level C code to perform logic model checking.
http://spinroot.com/gerard/pdf/cacm_2014.pdf
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