Engineering fads generally ought to be embraced with caution. However, the trend toward correct-by-construction development methodologies is one that can be adopted with some optimism, because even it when executed poorly, the result is usually preferable to that of the alternative.
For example, consider the case of a device with a PCI interface and a set of I/O mapped registers. Each register has an assigned I/O address. For example, the FUBAR register might have the address 0x0002.
In the simplest approach, the address of the FUBAR register is established in a specification or by mutual agreement. Every association with the address of this register is hard-coded to 0x0002. There may be multiple such associations in each of the hardware design, the device driver, the tests, the verification apparatus and the product documentation.
This first approach involves redundant design, because the same information is replicated in many design domains.
Another possible approach is to have a master include file that specifies the register locations. Filters translate this information into various formats such that it can be incorporated into each of the affected domains. Make(1) is used to keep generated files up-to-date.
This latter approach is correct-by-construction, because information derives from a central source that is correct by definition.
The approaches presented in the previous example produce equivalent results, and the second approach is clearly more complicated. Why, then, is correct-by-construction such a great idea?
The answer lies mainly in the fact that things change. For example, assume that the device is intended to serve as a drop-in replacement for another device that is discovered to have been surreptitiously using address 0x0002 already. Then FUBAR's address must change to some address that is not already in use.
Using the redundant design approach, every instance of FUBAR's address in every design domain must be changed. While this task is being carried out, the system is in an inconsistent state. Any instance that is overlooked will result in a bug. Furthermore, there may be instances of the constant 0x0002 in the design that have nothing to do with FUBAR, and changing any of those instances will also result in a bug.
On the other hand, using the correct-by-construction approach, only the master include file need be modified. Generated files are then updated automatically.
We have seen that the correct-by-construction approach involves additional up-front investment, but results in long-term rewards. One might conclude from this that short-term goals must be compromised in order to realize improvements. However, in my experience...
| Doing things correctly pays off sooner than you might otherwise expect. |
Automated tasks are generally faster than manual tasks. Even if the task is expected to be performed only once, it will be completed sooner if it is automated. In some cases, this fact alone makes correct-by-construction attractive.
For example, it might be easier to develop the infrastructure required for defining register addresses in a master include file, than to review a single snapshot of the redundant designs for register address inconsistencies.
The trouble with nontrivial manual processes is that one cannot usually afford to restart them. In the real world, unexpected late changes are likely to arise that will invalidate the results of past or pending efforts.
One way to address this problem is to prohibit changes to inputs of manual processes that have already begun. This too is expensive, especially when the affected input is simply wrong.
On the other hand, when a correct-by-construction methodology is employed, restarts become relatively inexpensive.
Perhaps the greatest advantage of correct-by-construction methods is that they are less likely to result in design errors, and that design errors that do exist are more likely to be discovered by static design analysis. As a result, the design is finalized sooner. Also, the same level of final design quality can be achieved with a less exhaustive verification effort.
While correct-by-construction is almost always a net win, there are still some common mistakes that one should avoid.
By far the greatest pitfall associated with correct-by-construction methodologies is that not all affected parties will necessarily understand them. Confused individuals are likely to subvert and/or undermine the methodology unintentionally, for example, by editing generated files.
This pitfall can usually be addressed by notifying and seeking consent from affected parties before changing methodologies or instituting a methodology that is not self-evident. Individuals who unconditionally refuse to acquire the skills necessary to follow best practices ought to be encouraged to seek employment elsewhere.
Just as there are costs associated with maintaining and supporting a product, there are costs associated with maintaining and supporting the methodologies used to develop a product. Alternatively, there are also costs associated with failing to do so. Extensibility beyond the product for which the methodology is initially developed is of particular concern.
The two common approaches to avoiding this pitfall are to outsource the development of the methodology to a vendor , or to follow good specification and development practices in developing the methodology.
Correct-by-construction methodologies usually preclude some of the low-level optimizations that can be performed when a redundant design approach is used. This problem is often overcome by the fact that one can utilize the time saved by not performing redundant design for performing high-level optimizations instead. Otherwise, one must consider whether the sub-optimality is justified by the other advantages associated with correct-by-construction methods.
One should avoid developing methodologies that are not clearly achievable a priori, because such efforts are costly and involve a great deal of risk. Similarly, one should not expect to rely on unproven purchased technology.
It is also a bad idea to apply correct-by-construction methods to problems that are trivially handled by redundant design methods. One should instead focus methodology improvements where they are most needed. Most likely, at any given point in time there are a number of areas within your organization that are in desperate need of methodology improvements.
Anders Johnson, last modified $Date: 2002/02/05 $