Correct By Design

Applying formal methods from the starting phase of Software Development Life Cycle ensures a product which is foolproof in all respects. This is what we mean as correct by design. Correct by design approach is different from formal verification which only proves that the product is operationally correct. Correct by design starts at the level of specifications. The domain could be hardware, software or genetic engineering (Lifeware). In the case of hardware, everything is clearly specified. The prohibitive cost of mistake in a hardware design has forced the engineer's to adopt rigorous formal techniques to validate the hardware. Formal methodologies have become mature and have become integrated engineering practices in hardware. The circuit produced needs to be correct, not because tests are run, problems are found and changes are made. It should work correctly the first time it is used (or tested) because it is designed and built right. Building right is neither an art nor a fluke, it is very much a mathematical activity. Systematic application of formal methods leads the designer to reach the same statement of the specification. The validation team then proves that the design meets the specification. In the critical cases, formal methods team and testing team take the same specification and meet the requirements of proving them correct. Genetic engineering is also following the same methods so that chances of error are eliminated.

On the contrary software development is asystematic and breaks down often in the absence of clear specifications. In correct by design approach, formal specification is mandatory for all applications. Having clear statement of the requirements leads to systematic and precise specifications. In the process of deriving precise requirements from loose requirements, incompleteness or contradictions get eliminated. When the precise specifications are achieved, it's complete and consistent in a mathematical sense, and thus traceably correct. It's easy to say whether a program is correct or not because the program has to perform according to the specification. In the instances of software development where specifications or statement of requirements are missing, it is very difficult to say whether the program is correct or not.

Software designers seldom put effort to be correct by design and to get it right the first time. This is because they want to keep the software flexible till the point of delivery so that any user requests can be accommodated till last minute. This flexibility is misused and often leads to poor quality of software. However, it is possible to achieve the same degree of correctness with software as with hardware. Software is no more complex than hardware. Software developers need to apply the same level of rigor of training and workmanship that is being done in hardware or genetic engineering (Lifeware). This would make software engineers develop products that's correct by design. "Good enough" software produced by hit and trial methods, testing and changing approach has to give way to correct by design approach.

Its a common notion that software developers can't produce software of high quality. Software glitches have become a common way of life. Be it mobile apps, banking solutions or web-portals. Glaring failures of ArianeV and death of patients due to over-exposure of radiation in certain medical machines have made everybody sit up and notice the software failures. The reason of often software failures is not spending enough effort and cost on the software design. Coding takes the center stage as a software engineering skill. To overcome these shortcomings in software it is important to spend as much money (effort and energy) up front for getting the design right. By applying the meticulous design process with exact (mathematical) primitives one can keep the impurities and errors out. The focus needs to be shifted from testing and release to up-stream for developing precise specifications. Code should be developed to meet these exact specifications. The essence is to follow processes that keep the errors out. The code thus developed is functionally verified to remove errors that were made during coding process only. Finally, testing is a statistical activity designed to demonstrate that there are no errors (rather than to find errors).

Another aspect is that engineers should be licensed and specifically certified for a particular domain. Compiler development, enterprise software development, mobile app development, CAD software development, medical software, embedded or mathematical software development, each is a different type of software from each other. One can shift domains if adequate skills and training is acquired. For example, developing a test tool is not same as developing a web-portal or developing a CAD tool is not same as developing a simulation tool. Formal methods are being extensively applied for control systems engineering and cyber-physical systems design. Many researchers are working on automatic synthesis of controllers from discrete specifications (languages, finite state machines, temporal logics, etc) for dynamic systems. The synthesized controllers describe both the control laws, discrete specifications as well as its “correct by construction” software implementation.

Correct by design approach is equally useful for simple as well as complex systems. Rigorous specification languages (Linear Temporal Logic, Computation Tree Logic), detailed design enunciation constructs(Finite State Machines, Binary Decision Diagrams, Multi-valued Decision Diagrams) and finally testing to prove the correctness, is the way to go. It will work the first time and every time. 

For views of Jesse Poore on this topic refer to following link:
http://ubiquity.acm.org/article.cfm?id=985613