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
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.