2 Introduction

Besides the difficulty for the average person to understand how to use formal methods, probably the next greatest criticism against formal methods is the absence of good measures for how much better formal methods make software. Increased quality is desirable; quality must be affordable. Few people would argue that formal methods are detrimental to software quality, but many people argue that for the added cost and difficulty-of-use, formal methods are not practical.

Further, formal methods advocates (or ``formal methodists'') for years have attacked the software testing community over well-known theoretical and practical weaknesses in various software testing techniques. Software testing suffers from an inability to exhaustively test, reliance on operational profiles and correct oracles, and an infeasibility to test to the higher levels of assurance. For the last decade, these two software engineering camps have fought instead of collaborated. (A classic example of this bickering was the debate between Boris Beizer and the ``Cleanroom'' advocates back in 1995 which is still waging in the presses [1].) Neither side claims to have the silver bullet, yet there are still those from each camp that seem to enjoy debating more than improving the state-of-the-art. Fortunately, the majority of practitioners seem eager to put aside personal preferences and find common ground.

This position paper addresses the need to fund research that marries both communities into a single community geared toward higher assurance software. In my opinion, formal methods are best suited to the earlier parts of the software engineering life-cycle, while testing is best left toward the end of the software engineering life-cycle. Because of this, the redundant work done by each different approach can be lessened by separating their use according to life-cycle phase and by learning where the key redundancies are. To our knowledge, this is still an open research issue, even though small advances in pre- and post-conditions embedded as testing assertions have been made.

Further, testing can augment the value-added by formal methods by demonstrating that the formal methods used really improved a program's quality. And as I said earlier, there are not good measures for how much better formal methods make software. Formal proofs throughout the life-cycle assert that certain behaviors cannot be exhibited. Such assertions need to be scrutinized. Software testing and several alternate testing methods can provide this scrutiny. By testing software that has been formally developed and proven, you are not just testing the software, but you are also testing the development processes. In this manner, testing provides a means for measuring the quality-gains afforded by formal methods. This measurement can begin to replace the anecdotal evidence that formal methods enable better software with empirical evidence.