Correct By Construction

"What is Correct-by-Construction software development?"

"Correct-by-construction approaches treat software development as a true form of engineering. [...] Similarly, a true software engineer constructs a mathematical model of his design before any code is produced. The model is used to reason about the proposed solution, ensuring that all required functionality will be delivered and the correct behavior exhibited. Testing is still performed, but its role is to validate the correct-by-construction process rather than to find bugs."

See: http://www.eschertech.com/products/correct_by_construction.php

[Seems to be popular largely in hardware, firmware and other related segments of the industry.]

---

"Correctness by Construction" by Praxis High Integrity Systems:

See: http://www.praxis-his.com/services/softwareengineering.asp

See: http://www.praxis-his.com/services/software/approach.asp

"seven key principles" at http://www.praxis-his.com/services/software/principles.asp

"The seven key principles of this approach are:

1. "Expect requirements to change.
2. "Know why you're testing.
3. "Eliminate errors before testing.
4. "Write software that is easy to verify.
5. "Develop incrementally.
6. "Some aspects of software development are just plain hard.
7. "Software is not useful by itself.

a. "To allow the developers to get from a set of requirements to an implementation.

b. "To allow the maintainers to understand how the implementation satisfies the requirements."

Case Study: "2.5 times as reliable as the space shuttle software, yet at a fifth of the industry standard cost." at http://www.praxis-his.com/services/software/casestudy.asp

---

http://www.esterel-technologies.com/company/overview.html

"The mission of Esterel Technologies is to provide correct-by-construction design tools that automatically generate defect-free implementations in software or HDL, and have as their core a rigorous and unambiguous specification."

---

Something mentioned in 'comp.risks' digest 23.75 -

 Date: Wed, 23 Feb 2005 21:35:30 -0000 
 From: "Martyn Thomas" <mar...@thomas-associates.co.uk> 
 Subject: Re: Component Architecture (Blaak, RISKS-23.74) 

"Well, I know one company that is willing to offer warranties on its software, free, because it uses a "Correct by Construction" approach that reduces the commercial risks to acceptable levels. They don't charge more for the development, either, because it doesn't cost them any more to work this way than industry norms.

"The company is Praxis High Integrity Systems: http://www.praxis-his.com

"And no - I don't have any financial links with them, although I did co-found a predecessor company."

---

In some ways, this reminds me of CleanroomSoftwareEngineering. CorrectByConstruction seems like a weak version of the CleanroomSoftwareEngineering. -- JeffGrigg

Oh; on the Praxis case study, on MULTOS. I did some work related to that product. Last I heard, it was a technical success (which supports their argument), but no one wanted to buy it. The product failed in the marketplace. Hmmm... -- JeffGrigg