Correctness by Construction
Correctness by Construction is a radical, effective and economical method of building software with high integrity especially for security-critical and safety-critical applications. It produces software with extremely low defect rates – fewer than 0.1 defects per thousand lines of code – with good productivity – up to around 30 lines of code per day.
At Praxis Critical Systems Anthony Hall and colleagues developed Correctness by Construction to unify a number of ideas:
It brings these strands together into a process framework and a set of principles for developing software intensive systems. It has been applied successfully in several projects such as the MULTOS CA, and is cited by the National Cyber Security Partnership as one of only three methods that are capable of producing software with the low defect rates needed for secure systems.
To learn more about Correctness by Construction, see