What is Correct-by-Construction software development?

Traditional approaches to software development rely on specifications written in English or another natural language, and hand-written program code. Sometimes a graphical notation such as UML is used to model the structure of the system and how it is used; but such models capture very little of the required behaviour, so that any code generated from them must be substantially reworked by hand. Either way, great reliance is placed on testing to uncover bugs in the software.

Correct-by-Construction approaches to software development treat it as a true form of engineering. For example, consider civil engineering. A civil engineer who intends to build a bridge constructs an accurate computer model of the proposed solution before laying the foundations.

Similarly, a true software engineer constructs a mathematical model of the design before producing any code. The model is used to reason about the proposed solution, ensuring that all required functionality will be delivered and the correct behaviour exhibited. Testing is still performed, but its role is to validate the correct-by-construction process rather than to find bugs.

Perfect Developer (also known just as PD) is a model driven development tool that uses the verified design-by-contract paradigm to develop software that is, indeed, correct by its method of construction. The Escher C Verifier (also known as eCv) is our tool for supporting a correct-by-construction approach to handwritten C code.