Read the article here: Code: Getting it Right

Hi Jack,

Good article. Indeed, making sure code is correct is a big question mark for many people. Yet a very important one. Bad design and coding has not killed as many people as badly constructed bridges, airplanes, cars etc have, yet therefore no (legally enforced) design verification takes place in (embedded) Software.

Formal verification by hand is, as you describe, a lengthy process. But that is not necessary. People who use ASD:Suite (from Verum: www.verum.com ) have a tool that enables the Software Architects and designers rapidly build, formally verify and automatically generate software for complex systems.

This patented software guarantees defect-free software. Companies like Philips (Healthcare / Medical Systems), NXP, Nandatech and many other use it already as defect-free software is very important to their customers.

Interestingly: they find that the total cost of development drops by 30% , where one would expect it to be more expensive given the defect-free guarantee. After-sales costs ('non-quality' cost) drops by 90%.

Take a look at: http://www.verum.com/technology/ to get an idea about the concept and it's abilities.

You are standing on the roof of high building - a rope hangs over the side - this is the only way down.

A Sales Manager and a leading academic approach you. The Sales Manager has the latest tool for formally proving the safety of the rope. The academic advises the applicability of formal methods have been oversold for decades.

You are given the option of testing the rope with a resentative weight, or proving its safety using predicate calculus.

See you on the ground?

Not to deny the power of formal methods... but having run into numerous cases of coding that met design specifications perfectly, yet did things that were astoundingly bizarre... who is going to mathematically prove that the specification was "right" in the first place?

“Getting it Right”, for who or what? Q&A? IV&V? Requirements? Specifications? Formal Methods?
We need to be “Getting it Right” for the USERS! (It their lives that are at risk!)

Most of our embedded S/W is drop shipped. (User problems are “user problems” until they prove otherwise.) If we do respond to user problems, we are faced with the expensive and time consuming task of trying to re-create the problem, from limited and often inaccurate data. This is probably why we tend to live in our own little world disconcerted and isolated from the users. (Just look at how our software support organizations are designed to work for us and not the users.)
We will not even try to close this gap between us and the users. If we did, we would see the true reliability of our software. THIS IS THE FUNDAMENTLY PROBLEM STANDING IN THE WAY OF RELIABLE EMBEDDED SOFTWARE!

If you think embedded software reliability is improving, don’t look at what the software development environment is (or is not) putting in the executable file. You could see a “memory++;” line of code that translates into:
xxxxxxxx0: xx xx xx xx ld.w r8,pc540
xxxxxxxx4: xx xx ld.w r8,r80x0
xxxxxxxx6: xx xx ff ff sub r9,r8,-1
xxxxxxxxa: xx xx xx xx ld.w r8,pc530
xxxxxxxxe: xx xx st.w r80x0,r9
If you think this is strange, you should see what the “memcpy” function (from the development environment) is doing!