Lambda the Ultimate

inactiveTopic Correctness by Construction: Better Can Also Be Cheaper
started 3/12/2002; 10:31:00 AM - last post 3/25/2002; 11:28:08 AM
Ehud Lamm - Correctness by Construction: Better Can Also Be Cheaper  blueArrow
3/12/2002; 10:31:00 AM (reads: 1689, responses: 3)
Correctness by Construction: Better Can Also Be Cheaper
(via comp.lang.ada)

Correctness by Construction: Better Can Also Be Cheaper. Peter Amey, Praxis Critical Systems. CrossTalk Magazine, March 2002

For safety and mission critical systems, verification and validation activities frequently dominate development costs, accounting for as much as 80 percent in some cases. There is now compelling evidence that development methods that focus on bug prevention rather than bug detection can both raise quality and save time and money. A recent, large avionics project report­ ed a four­fold productivity and 10-fold quality improvement by adopting such methods. A key ingredient of correctness by construction is the use of unambiguous programming languages that allow rigorous analysis very early in the development process.

The main focus of the paper is the SPARK Ada toolset, but the paper raises issues that are of general interest. The key notion is that of the benefit of a precise language or lan­guage subset. This is important since it allows for tool support.

The paper discusses the building of the avionics of the Lockheed C130J (the Hercules II Airlifter), and the costs of achieving level A DO-178B certification (the DO-178B being the prevalent standard against which avionics software is certified).


Posted to Software-Eng by Ehud Lamm on 3/12/02; 10:44:48 AM

Ehud Lamm - Re: Correctness by Construction: Better Can Also Be Cheaper  blueArrow
3/12/2002; 10:49:19 AM (reads: 868, responses: 0)
Perhaps one more quote...

The savings arose from avoiding testing repetition by eliminating most errors before testing even began.

Chris Peterson - Re: Correctness by Construction: Better Can Also Be Cheaper  blueArrow
3/12/2002; 9:44:11 PM (reads: 843, responses: 0)
One of the paper's footnotes points to an interesting web site: www.mirsa.org.uk, the UK Motor Industry Software Reliability Association. They have defined a "safe" subset of C for use in automotive and embedded systems. There is very little literature on their site, though I would be interested in reading more.

Many of their C restrictions do not seem like they could be enforced by a hypothetical compiler without extra annotations (such as LCLint). For example: "The right hand operand of a && or || operator shall not contain side effects." They then go on to recommend the use of ?: over complicated if statements. I find myself using the ?: operator increasingly often to write more functional-like C code. :)

Ehud Lamm - Re: Correctness by Construction: Better Can Also Be Cheaper  blueArrow
3/25/2002; 11:28:08 AM (reads: 745, responses: 0)
The correct url: http://www.misra.org.uk/