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:
- rigorous requirements engineering
- the use of formal methods
- a systematic, multi-view approach to system architecture
- static analysis using SPARK
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.
To learn more about Correctness by Construction, see
- a short overview of the principles
- a fuller description