Are you interested in how functional programming can be leveraged to make embedded-systems programming easier and more reliable? You are not alone. For example, check out what’s been happening in just the past couple of years.
- Programming the Arduino micro-controller with Atom/Haskell.
- The Atom eDSL language itself.
- The Feldspar language for DSP (embedded in Haskell).
- Writing a DO178B-compliant compiler in Ocaml (presented at ICFP’09).
- … And others.
In the January 2010 copy of IEEE Computer, David Parnas published an article, “Really Rethinking ‘Formal Methods’” (sorry, you’ll need an IEEE subscription or purchase the article to access it), with the following abstract:
We must question the assumptions underlying the well-known current formal software development methods to see why they have not been widely adopted and what should be changed.
I found some of the opinions therein to be antiquated, so I wrote a letter to the editor (free content!), which appears in the March 2010 edition. IEEE also published a response from David Parnas, which you can also access at the letter link above.
I’ll refrain from visiting this debate here, but please have a look at the letters, enjoy the controversy, and do not hesitate to leave a comment!
, or one-in-a-billion, is the famed number given for the maximum probability of a catastrophic failure, per hour of operation, in life-critical systems like commercial aircraft. The number is part of the folklore of the safety-critical systems literature; where does it come from?
First, it’s worth noting just how small that number is. As pointed out by Driscoll et al. in the paper, Byzantine Fault Tolerance, from Theory to Reality, the probability of winning the U.K. lottery is 1 in 10s of millions, and the probability of being struck by lightening (in the U.S.) is more than a 1,000 times more likely than
So where did come from? A nice explanation comes from a recent paper by John Rushby:
If we consider the example of an airplane type with 100 members, each flying hours per year over an operational life of 33 years, then we have a total exposure of about 107 flight hours. If hazard analysis reveals ten potentially catastrophic failures in each of ten subsystems, then the “budget” for each, if none are expected to occur in the life of the fleet, is a failure probability of about per hour [1, page 37]. This serves to explain the well-known requirement, which is stated as follows: “when using quantitative analyses. . . numerical probabilities. . . on the order of per flight-hour. . . based on a flight of mean duration for the airplane type may be used. . . as aids to engineering judgment. . . to. . . help determine compliance” (with the requirement for extremely improbable failure conditions) [2, paragraph 10.b].
 E. Lloyd and W. Tye, Systematic Safety: Safety Assessment of Aircraft Systems. London, England: Civil Aviation Authority, 1982, reprinted 1992.
 System Design and Analysis, Federal Aviation Administration, Jun. 21, 1988, advisory Circular 25.1309-1A.
(By the way, it’s worth reading the rest of the paper—it’s the first attempt I know of to formally connect the notions of (software) formal verification and reliability.)
So there a probabilistic argument being made, but let’s spell it out in a little more detail. If there are 10 potential failures in 10 subsystems, then there are potential failures. Thus, there are possible configurations of failure/non-failure in the subsystems. Only one of these configurations is acceptable—the one in which there are no faults.
If the probability of failure is then the probability of non-failure is So if the probability of failure for each subsystem is then the probability of being in the one non-failure configuration is
We want that probability of non-failure to be greater than the required probability of non-failure, given the total number of flight hours. Thus,
which indeed holds:
Can we generalize the inequality? The hint for how to do so is that the number of subsystems () is no more than the overall failure rate divided by the subsystem rate:
This suggests the general form is something like
Subsystem reliability inequality:
where and are real numbers, and
Let’s prove the inequality holds. Joe Hurd figured out the proof, sketched below (but I take responsibility for any mistakes in it’s presentation). For convenience, we’ll prove the inequality holds specifically when but the proof can be generalized.
First, if the inequality holds immediately. Next, we’ll show that
is monotonically non-decreasing with respect to by showing that the derivative of its logarithm is greater or equal to zero for all So the derivative of its logarithm is
Let , so the range of is
Now we show that in the range of , the left-hand side is bounded below by the right-hand side of the inequality.
Now taking their derivatives
Because in the range of , our proof holds.
The purpose of this post was to clarify the folklore of ultra-reliable systems. The subsystem reliability inequality presented allows for easy generalization to other reliable systems.
Thanks again for the help, Joe! Read the rest of this entry »