Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Not sure what means that most of the C code is auto generated. From what?


They make models of the software before writing any code, and a lot of the code can be generated from the models. There's a guarantee that if the model is correct so is the code. Or, you don't have to check that your hand-written C actually matches the system you were building.


This is really key. The guarantees provided by modeling systems are of limited value if the translation between model and runnable code involves manual labor.


What do you mean by model?


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


Compilers that are verified/validated (in some sense):

http://compcert.inria.fr/compcert-C.html

http://www.cs.utah.edu/~regehr/papers/

http://lambda-the-ultimate.org/node/4571

-------------

The "Related Work" section in this UVa dissert probably most closely answere your question

http://www.cs.virginia.edu/~jck/publications/Xiang.Yin.disse...


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!


Probably from Simulink.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: