[alandarev]

Software contractor for Airbus and Rolls-royce here.

All safety critical software (every piece of code ran on-board is safety critical the least) in aerospace needs to pass the DO-178 standard [1].

That is far more serious than standard unit tests you are used to in node.js applications. Generally speaking, to develop a piece of code under that standard it takes 20% of time to write the code, and 80% to testing, and enormous amount of documentation (that is optimistic estimation, usually worse).

Quoting speaker from DO-178 training course I attended:

   People often ask us. "How do we know the standard works?"
   We give this answer: "We do not know. But there have been zero crashes due to software issues since introduction"

If this crash confirms the cause to be a software bug, that is something much bigger than an airplane crash - a huge punch to the whole federal aviation administration.

[1] - http://en.wikipedia.org/wiki/DO-178B

[jonnycowboy]

I also work in aerospace software. Following DO178 certainly does not guarantee that there will be no software bugs. The point of DO178 is to follow a process that will _minimize_ the number of bugs by having adequate peer review processes throughout the requirement definition, coding, integration phases, in addition to the testing you mention above. Testing DO178 only tests that the code follows the requirements. If your requirements are fucked, so are you.

[gvr]

That is certainly one source for error. There are many. Another is that testing does not give you exhaustive coverage of the state space just because each branch of the code is visited.

The standard does mention "formal verification/methods/proof" but to my knowledge it's rarely been used extensively.

[wyldfire]

Mathworks makes a sat solver kinda product that does those kinds of proofs. Pretty interesting concept, IMO.

[userbinator]

The target catastrophic failure rate there is 1 in a billion hours, which doesn't seem all that high to me... there are over 100000 flights a day[1], and the average length of one is well over an hour, so in one day all the aircraft in the world have accumulated a total of over 2.4 million hours in operation. If each flight was only an hour long, that's 417 days to 1 billion total hours, and if the failure rate really was 1 in a billion we'd expect to see one of these happen at almost yearly rates.

The actual failure rate of software to this standard seems to be at least two orders of magnitude higher.

[1] http://www.garfors.com/2014/06/100000-flights-day.html

[peeters]

Where is the "actual failure rate" number coming from?

[branchan]

How does 100k flights a day equal 2.4 millions hours of operation if each flight was on average 1 hour?

[grkvlt]

Yeah, confused. If we assume a two hour average flight, we get 365 * 2 * 100K = 73M hours/year so one failure per 1G hours is one failure in 1000 / 73 = ~14 years.

[calebm]

I wrote (non-critical) software for the A400M. I don't think that standards like DO-178B necessarily lead to higher quality code; my experience was that 80-90% of time was spent doing documentation, testing, and in general, trying to prove that the software was going to work right, leaving the engineers with very little time to write the actual software...

[Jtsummers]

What processes did you and your coworkers use for writing up your requirements, design, test procedures, etc. (Basically, the DO-178B/C artifacts.) IME, too many times groups use Word and Excel, and collaborate via email. Version control is, "I think CM has received my latest revision". Using better tools (requirements management software) would eliminate a lot of this overhead. At a former employer we were moving to DOORS on all new projects. They were able to spend much more time on development and analysis and less time on documenting and checking documentation because the process was smoother. They weren't editing 1k page documents, they were editing a collaborative document backed by a database, not unlike a wiki. I could edit one section, and you could edit another at the same time. No risk of merge conflicts, no risk of your update replacing mine.

[crististm]

DOORS is just a glorified database with a text editor and schema for tracking change requirements. I found it lacking even at this.

[Jtsummers]

Not saying it was great, but it was a hell of a lot better than Word + Excel. Probably a lot of better tools out there, but it's been a while since I've needed to use them so I'm no longer familiar with what's available.

What made it better:

Concurrent editing. Only one person at a time was modifying any section, but two or more sections could be edited by a group of people.

Version control baked in. VC is awesome, reducing friction means that it actually gets used. Checking in/out sections was just part of the process.

Automatic traceability matrices. These are not easy to make by hand. That way is error prone and tedious. It's also hard to verify. With DOORS we were able to generate these automatically. Verifying them was relatively painless because we weren't flipping through several 1k page documents to make sure things actually matched, we could easily skip to only the applicable parts of any document. The main error that it didn't reduce was when a requirement didn't get linked to every test case or design feature that it should've been linked to.

Again, probably better tools out there than DOORS (at the time, or hopefully by now). But it's a lot better than what most offices do with either post hoc document generation or ad hoc generation with Word + Excel.

[sliverstorm]

in general, trying to prove that the software was going to work right, leaving the engineers with very little time to write the actual software...

Sure sounds like the way it should be to me. Maybe it needs to be made easier to prove your software is correct, but to me it seems like for systems like airplanes, code that cannot be proven correct is worthless.

Considering most programmers are said to produce 6 lines of good code a day, maybe it's not even actually slower in the end if the formal verification process filters out every other line you would have written that day.

[calebm]

It's not a bad thing to put in quality assurance measures in place. It's a bad thing, though, if so much time is spent on QA, that there you are rushing to write the actual code. Rushed coding does not produce quality.

[emp_zealoth]

Every time i read about stuff like that i get mad. Attitude regarding software is just criminal. You wouldn't let internt/inexperienced people design mechanical parts of the plane. Engineers are bound by standards regarding everything. Materials, mechanical couplings, documentation. when i design a machine, i can't scribble it on a napkin and ship it. Why is it acceptable for idiots to write messy, unintelligible code? When i create a mechanical drawing, i am bound by rules how to draw it. With coding everyone has their own ideas. When i design a machine i have to make sure it will work, period. Calculations to be done no matter how i don't have to spend thousand of man-hours fiddling with it to see if it works as intended

the apologetic attitude needs to stop. programs are just complicated machines and should be treated as such not some mystical voodo that will be broken no matter what

[tormeh]

I think you're glorifying engineers here. They're a lot more careful, but they don't have some fairy pixie dust of rigor that makes everything work perfectly.

[belorn]

How does liability work, and do Airbus have access to the source code? I assume that if a "bug" was found in the architectural blueprint for a plane it would be the manufacturer who in the end is responsible for not finding it, but they would naturally have full access to the blueprint when making the plane. Is the same true when developing the custom software for the plane?

[luch]

Well it's military airplane so it's a bit special here, usually it's the costumer (i.e. the army) which is liable if the plane has passed the final tests.

However it's a complete different matter for civil airplanes : it's the lead dev/project manager which is liable for life for what he has shipped. For example, a retired engineer from Airbus was heard in trial for the Concorde accident in France in 2000.

[TeeWEE]

I'm quite baffled at the fact that this standard does not include formal verification of the software models used.

Formal verification and state space analysis can prove that the software "model" will not fail. State space exploration of the actual implementation is actually often not feasible due to the enourmous amount of states.

So my question: Are you doing formal analysis of the software models/designs? I know they are using it in software used in space crafts / nuclear power plants.

Reference: - http://ti.arc.nasa.gov/m/profile/dimitra/euromicro-share.pdf - http://javapathfinder.sourceforge.net/

[sfrank]

The DO-178B/C explicitly does not specify how verification is done but describes the properties that are expected of the verification evidences that you submit to the certification authorities; so formal verification is perfectly fine as one item on your verification check list. In particular DO-333 amends DO-178C with specific topics concerning formal methods.

For example Astree [1] has been developed for decades now, with Airbus as one of the major sponsors.

[1] http://www.astree.ens.fr/

[tedunangst]

What is the largest piece of code you have formally verified?

[bglazer]

The seL4 mircrokernel is comprehensively formally verified and is marketed towards aerospace applications.

https://sel4.systems/

[castell]

Which programming language is commonly used there? Ada, C, C++, JOVIAL, Asm?

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

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

[jcadam]

Really, you'd want to use Ada for something like this (The language has survived specifically because it's managed to carve out a niche for itself in aerospace).

I once worked on satellite systems using Ada95 and Ada2005 (Ada is definitely not dead). The language is a pain to use but is impressive in that it catches more crap at compile-time than anything else I've seen.

[progman]

> Ada is definitely not dead

True. More information: http://www.ada2012.org

[lamby]

With that kind of coding-to-testing-and-documentation ratio, does it even matter?

[TheLoneWolfling]

Yes, definitely.

For a quick example, there are many languages where you cannot accidentally run off the end/start of an array, barring a compiler error.

With a language like C / C++, it's possible. Not probable, given that sort of testing. But possible nonetheless.

Some languages are also easier to test than others, partially because of this, partially because of other issues. For instance, in some languages you can guarantee at the language level (again, barring compiler errors) that something won't be modified. (Like const, but actually working.)

[gsnedders]

Yes. The more the type-system encodes the more the type-checker (in the compiler) proves for you. No matter how much testing you have, nothing will ever come close to proving properties.

[UnoriginalGuy]

Yes. Some languages are better at scoping than others. Functional languages are easier to test because they have more confined scope.

[tjbiddle]

Then to add to it, what are tests written in?

[agumonkey]

I've seen this first hand, unfortunately this doesn't escape the hiring market reality. Many documents and source files are littered with (very) bad code from an 3 months employee that couldn't do better before leaving considering the extreme size of the project.

I wonder if someone can pull an #ElonMusk on the DO-178 to slim things down in order to have better control.

ps: planes fly with bugs, see the DreamLiner, Airbus ones aren't free from them either, employees know this. (I guess they travel by train)

[ExpiredLink]

> I guess they travel by train

The train brake control systems are written in ... C.

[agumonkey]

Yeah but usually when two trains collide, you don't have the time to see it coming.

[mrmondo]

Is the code is available for review outside the operating constraints of the system that designed it - I.e. Is it open source?