[shepardrtc]

Nowadays, its C/C++. In the past it was Ada (at least in the US). Ada was created specifically for this sort of thing (and was actually a requirement for certain projects), but it never gained popularity so companies would just petition the government to use C/C++ instead. Its a shame, too. Ada is fantastic if you want to avoid bugs. I wish more people would give it a chance.

On the other hand, I also wonder why people don't think of using Erlang for something like this. The VM is designed for a ridiculous amount of uptime, it has a supervisor tree that can monitor and restart failed processes, and it can interface with C/C++. A rock-solid VM should be running and monitoring life-safety systems.

[Jtsummers]

Erlang's model is entirely appropriate, but the language and VM aren't. This code is often running on small embedded chips (so you'd need to port the VM) and the software has hard real-time requirements, which the Erlang VM is not (currently) set up to handle, nor would it necessarily be able to achieve on the commonly used processors. Another strike against the language (as much as I love it) is that it's dynamically typed. That's less appropriate for this sort of software. There are static analysis tools for Erlang that mitigate this, but it's still an issue. Large classes of bugs and errors can be eliminated or minimized with statically typed languages or with static analysis tools if they're well integrated into the build process. A real-time, statically typed language with Erlang's semantics and compiled to native binaries would be a boon, however.

I'll speak to the 787 avionics system. It used a system of channels/buffers and processes very much like what Erlang and Go use for interprocess communication (I'm trying to remember now if channels could be received in multiple processes like Go or if only a single process could receive like in Erlang). This was an excellent model for what we were doing, and really for a lot of systems this sort of CSP and actor style model maps well.

[tormeh]

Using C/C++ on these projects is idiotic. If Airbus used C/C++ then they deserve all the financial loss in the world. They have blood on their hands.

[lambdaelite]

Keep in mind they don't use C/C++. They use C/C++ with a coding standard (like MISRA), static analysis tools, validated compilers, development processes incorporating change control, documentation, verification and validation, etc.

What alternative are you suggesting?

[progman]

I know that Ada compilers are 100% verified correct but is there really any validated C++ compiler? Which one?

AFAIK (partial) assurance in C/C++ can only be handled by additional testing tools, Frama-C for instance.

I agree that C/C++ should not be used for security applications. Ada is a much better choice because it was designed for security.

[lambdaelite]

Not sure if I'm understanding your question correctly, but Wind River claims their Diab compiler is validated by TÜV NORD and is has been used for stuff up to SIL4.

In fact, they (http://windriver.com/products/product-overviews/PO_Diab_Comp...) say:

  Diab Compiler has been a reliable code generation tool for
  avionics products certified for DO-178B, products for the
  nuclear market certified to IEC 60880, railway applications
  certified to EN 50128, and industrial products certified
  to IEC 61508, and is now qualified for use in automotive
  applications certified to ISO 26262.

Ada does have some built-in advantages, but I think my point still stands: the language is a small part of the entire SDLC, and I don't think it's the most important part.

[castell]

Is TÜV Nord/Sued known for extensive software checking?

[CHY872]

Are you sure that Ada compilers are verified correct?

I'm pretty sure that the only industrial formally verified compiler is CompCert (for C), though I could be wrong. The motivation for CompCert was certainly that Airbus wanted such a compiler.

Ada wouldn't be a better choice simply because it's designed for security. It'd be a better choice if it turned out better in practice. I've read some of the studies that have been done, and I haven't found them convincing.

Requiring additional tools just isn't a problem, if it works well. Don't criticise the process, criticise the result.

[tormeh]

Ada, of course. Are you saying it wasn't at the forefront of your mind? If I sound patronizing it's because I am.

[lambdaelite]

As I said elsewhere, Ada does have some very nice built-in advantages, but I think my point stands: the language is a small part of the entire SDLC, and I don't think it's the most important part.

The focus on languages instead of the SDLC is telling, I think.