What is the Mars Curiosity Rover's software built in?

I don't know if there is a PDF. The media player is interesting, though, in that it's actually just some javascript that loads a sequence of stills at the appropriate time, and if you look at the source, you can write, say, a python script to download all the images, which I did. When I get home, I'll see if I can find it.

A formal model of how the software is supposed to behave. Models can be proven to have certain properties (e.g. deadlock-free, cruise control always turns off when brake is hit), while with software you're usually limited to testing. A proof guarantees that the software works for all possible inputs, whereas when testing only some inputs are tried.

To model individual processes, one could use automata, for interaction of processes there are process calculi.

http://en.wikipedia.org/wiki/Formal_methods

I wrote it[edit: by which, I mean the answer containing the sentence in question], and I'm not 100% sure, although there probably is a separate presentation in that year or a different year that describes their auto-generation process. I know that it was a popular topic in general at the FSW-11 conference.

Simulink is a possibility. It's a MATLAB component popular among mechanical engineers, and therefore most navigation & control engineers, and allows them to 'code' and simulate things without thinking they're coding.

Model-based programming is definitely a thing that the industry is slowly becoming aware of, but I don't know how well it's catching on at JPL or if they would have chosen to use it when the project started.

The third and most likely possibility is for the communication code. With all space systems, you need to send commands to the flight software from the ground software, and receive telemetry from the flight software and process it with the ground software. Each command/telemetry packet is a heterogeneous data structure, and is is necessary that both sides are working from the exact same packet definition, and format the packet so it is correctly formatted on the one side, and parsed on the other side. This involves getting a whole lot of things right, including data type, size, and endianness (although the latter is usually a global thing, you could have multiple processors onboard with different endianness).

But that's just the surface. You need lots of repetitive code on both sides to handle things like logging, command/telemetry validation, limit checking, and error handling. And then you can do more sophisticated things. Say you have a command to set a hardware register value, and that value is sent back in telemetry in a particular packet. You could generate ground software that monitors that telemetry point to ensure that when this register value is set, eventually the telemetry changes to reflect the change. And of course, some telemetry points are more important than others (e.g. main bus current), and are designated to come down in multiple packets, which involves extra copying on the flight side and data de-duplication on the ground side.

With all that, it's much easier (in my opinion) to write one collection of static text files (in XML, csv, or some DSL/what-have-you), run them through a perl/python script, and presto! Code!

OK, here's the script I had hacked together. It (or some previous version), successfully downloaded all of the images, and a timings.txt. It was then supposed to create a movie file of each slide of the appropriate length, concatenate them all, and add the audio. But my VM kept crashing, and then I never had time to get back to it. Plus, the movie file ended up being very large. But if you have python 2.7.2+, you can run it and grab the images.

https://github.com/nsp/gazpacho

I bet he was. I also bet that MSL also has some Java on it since JPL is all about code reuse.