[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

[Jayschwa]

I worked at an avionics contractor for a number of years and that mirrors my experience as well. On Level A projects, the process was at least followed, but it was often under tight stressful deadlines. Testing was frequently off-shored to save money, but often resulted in low quality tests that had to be reworked at the last minute by in-house engineers.

The state on a later Level C & D project was in worse shape: bloated architecture, lots of requirements churn, little to no peer review, one unrealistic deadline after another, and mandatory overtime for large periods. It was not an environment conducive to thoughtfulness or quality. I finally got fed up and quit.

[snom320]

Did you work specifically on the engine controllers? Have you considered speaking to the accident board about this?

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

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

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

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

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

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

[lamby]

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

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

[mrmondo]

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