4 ms·
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 corre
by mgurlitz 14y ago
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.
- RodgerTheGreat 14y agoThis is really key. The guarantees provided by modeling systems are of limited value if the translation between model and runnable code involves manual labor.
- msh 14y agoWhat do you mean by model?
- andor 14y agoA 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 http://en.wikipedia.org/wiki/Formal_methods
- gtani 14y agoCompilers that are verified/validated (in some sense): http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html http://www.cs.utah.edu/~regehr/papers/ http://www.cs.utah.edu/~regehr/papers/ http://lambda-the-ultimate.org/node/4571 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.dissertation.pdf http://www.cs.virginia.edu/~jck/publications/Xiang.Yin.disse...