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.
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.
