Verification
A great deal of effort, money, and time are spent in the creation of software and hardware, and much also depends upon their correct performance. It is not at all uncommon for there to be situations where the loss of life and property would be the result of non-performance or incorrect performance of either hardware or software. Testing of the program or hardware prototype is not itself sufficient to guarantee correct behavior--how can we be certain it behaves correctly under all possible operating conditions? This can often be difficult to determine from testing alone, as operating conditions may vary widely, and sometimes may not be fully known in advance. It is also possible that certain very rare combinations of factors may occur to disrupt performance, but that these combinations may not be forecast in advance.
Thus, it becomes highly advisable to have a rigorous method by which one can be assured that an artifact will indeed work just the way it is required to. The application of such a method to one's design or ideas would enable there to be a formal assurance, for example, that a certain program is as correct in its behavior as is the statement of the Pythagorean theorem in geometry. Anyone who wished to verify this claim would be able to do so by following the formal proof, just as one could verify the correctness of the Pythagorean theorem.
The discipline by which one determines, in a mathematical fashion, the correctness of a design or concept, is called verification. "Verification' is a broad concept, covering both hardware and software verification, and it uses many distinct and important tools and techniques. In practice, most researchers in the field actually specialize in either software or hardware verification, and often use certain specific tools and techniques such as temporal logic, model checking, and so on.
Verification is obviously a concept much in demand for the sake of being able to produce sensible artifacts that do just what is desired of them and nothing else. It is also important in a legal sense, because issues of legal liability could be involved in case of artifacts that do not perform correctly and cause damage or injury. Verification is also important in an economic or financial sense, because investors may be unwilling to risk supporting a project about which there are no formal guarantees. Being able to formally verify that a certain concept is sound is also likely to help avoid blunders along the way that may lead to wastage of money and effort.
In order to verify that a certain program or a piece of hardware is going to perform as it should, it is necessary for one to first be able to describe it formally. Such specification of an artifact or a system should capture its essential characteristics in a sensible way, while leaving out inessential features that are not pertinent as to its design correctness. For example, for certain applications, the memory size and CPU speed of a computer may be relevant while its power consumption and external appearance may not be; accordingly, the former qualities should be included and the latter should not be, in the specification. Sometimes the determination of exactly what characteristics are essential for correct performance can be tricky to find out, for which reason formal verification can be a significant but incomplete step toward complete assurance. A well-known quote from the famous computer scientist Donald Knuth says, "Beware of bugs in the above code; I have only proved it correct, not tried it."
Unfortunately, verification proofs are also very often tedious to read and difficult to understand; even if the program to be verified is not too long, it is just likely as not that the proof of its correctness will be. For this reason, a major push in contemporary research is for tools to automate the obtaining of verification proofs, with human involvement being kept to a minimum. Major accomplishments have already occurred in this area, and it is now common practice to use an automated system that will mechanize many of the boring and routine aspects of verification.
Verification is thus an important part of software and hardware design. However, the state of the art in verification is yet a long way from being totally satisfactory. Much work needs to be done to enable the complete automation of verification proofs, and indeed, at this time the formal verification of complex systems is often so difficult that complete verification is considered to be too expensive and unjustifiable. Only partial verification, or verification of chosen parts or components, is attempted. Newer advances in the field should certainly help with these problems.
This is the complete article, containing 772 words
(approx. 3 pages at 300 words per page).
