Spinroot

A forum for Spin users

You are not logged in.

#1 2014-02-02 00:12:03

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

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

Board footer

Powered by FluxBB