The Ganssle Group logo


Bookmark and Share
The logo for The Embedded Muse For novel ideas about building embedded systems (both hardware and firmware), join the 25,000+ engineers who subscribe to The Embedded Muse, a free biweekly newsletter. The Muse has no hype, no vendor PR. It takes just a few seconds (just enter your email, which is shared with absolutely no one) to subscribe.

Getting it Right

Summary: A new OS has been proven to be correct using mathematical proofs. The cost: astronomical.

Poll question: Bug metrics: - We track them carefully - We mostly track them - Anecdotal measurements - No metrics

How good is your code?

Most of us have no quantitative idea. A few outfits measure bug rates, but, as been often observed, an apparent absence of bugs does not mean the code lacks defects.

While safety-critical code is often better-tested, and sometimes better-designed, than average industrial software, testing cannot prove the absence of bugs. According to Adams, N.E "Optimizing preventive service of software products", IBM Journal of Research and Development, 28(1), p. 2-14, a third of all software faults take more than 5000 execution-years to manifest themselves. That's encouraging for those of us not planning to challenge Methuselah, but graphically illustrates the inadequacy of testing.

Some operating systems are certified to extremely-high levels of reliability and/or security. To my knowledge none have been completely proven using the most rigorous formal methods (some, like Green Hills' Integrity, certified to EAL6+ against a particular protection profile, come close). Until now. According to http://nicta.com.au/news/current/world-first_research_breakthrough_promises_safety-critical_software_of_unprecedented_reliability, NICTA's Secure Embedded L4 microkernel has been completely proven correct using formal methods. That's quite an achievement.

But more interesting is the stunning cost required to make the proofs. The OS comprises 9,300 lines of code, of which 7,500 have been verified. The cost of verification: 25 to 30 person years of work! At a loaded cost of $200k/person year, that's over $5m, or about $700 per line of code. Since most firmware runs $20-40 per line of code (this covers the entire cost of the project), formal verification is twenty times the cost of writing the stuff in the first place.

Actually, $700/LOC is cheaper than one might think. Green Hills apparently spent about $1000/LOC (see http://www.sdrforum.org/pages/sdr04/3.5%20Security%20%20Dillinger/3.5-3%20Hart.pdf) to achieve their EAL6+ validation, which is not as strong as a proof as what NICTA claims. NICTA themselves believe EAL6 certification would run about $10,000/LOC (http://ertos.nicta.com.au/research/l4.verified/numbers.pml). That's quite a range; even at the low end it's gobs of cash.

They found 144 bugs while formally proving the OS. That's about a 2% rate, which suggests very little testing was used prior to the proof.

So- how good is your code? How do you insure it's close to being right?

Published October 14, 2009

New and Noteworthy

Do you need to reduce bugs in your firmware? Shorten schedules? My one-day Better Firmware Faster seminar will teach your team how to operate at a world-class level, producing code with far fewer bugs in less time. It's fast-paced, fun, and covers the unique issues faced by embedded developers. Here's information about how this class, taught at your facility, will measurably improve your team's effectiveness.

New Video! Jack's latest video shows how to measure idle time. Here's a list of all of Jack's videos.

Public seminars! Jack is presenting his Better Firmware Faster seminar in Baltimore, San Jose, and Germany in November. Join the 5000+ developers who have learned more efficient ways to develop embedded firmware. More info here.



Advertise here! More info.

The Ganssle Group - info@ganssle.com - Copyright The Ganssle Group - Contact info here

Interested in advertising with us? More information here.