I came a cross this paragraph in "Model-Based Engineering of Embedded Real-Time Systems" book
Model-based design is considered by many as a suitable approach to overcoming these limits, particularly in the embedded systems domain. One of the expected advantages of this approach is the ability to exploit correct-by-construction incremental design processes, which rely on extensive use of automated transformations and synthesis, as well as formalized computer-based analyses of correctness
Could you please clarify the highlighted sentence by giving some examples because I didn't understand what does that mean?
The following is a quote from Master thesis of Eric Miotto:
Challenges in the Integration of domain-specific and scientific bodies of knowledge in Model-Driven Engineering
the point is that the system is already implemented and it is needed to return again to its design and construction to fix the problems – this can be very expensive and there is the risk to introduce new unanticipated bugs. We can name this approach as construction by-correction– a working system is obtained by means of repeated constructions and verification.On the contrary, in other mature engineering fields, the system (let it be a bridge or a chip) is not immediately built, but it is first modeled using patterns and solutions apt for its class, devised so to permit the verification of relevant properties. This way it is not necessary to build the system to detect its defects, but they can be found in the design phase, with the great advantage that it is known exactly how to deal with them and that further problems will be properly detected thanks to the employed patterns and solutions. The construction of a system is started only when the design meets all the requirements (to a certain degree). We can refer to this approach as correctness-by-construction – a working system is built by means of proven modeling and design.