Formal methods for conformance testing: Theory can be practical

Abstract

Although testing is the most widely used technique to control the quality of software systems, it is a topic that, until relatively recently, has received scant attention from the computer research community. Although some pioneering work was already done a considerable time ago [Cho78,GG83,How78,Mye79], the testing of software systems has never become a mainstream activity of scientific research. The reasons that are given to explain this situation usually include arguments to the effect that testing as a technique is inferior to verification — testing can show only the presence of errors, not their absence — and that we should therefore concentrate on developing theory and tools for the latter. It has also been frequently said that testing is by its very nature a non-formal activity, where formal methods and related tools are at best of little use. The first argument is incorrect in the sense that it gives an incomplete picture of the situation. Testing is inferior to verification if the verification model can be assumed to be correct and if its complexity can be handled correctly by the person and or tool involved in the verification task. If these conditions are not fulfilled, which is frequently the case, then testing is often the only available technique to increase the confidence in the correctness of a system. In this talk we will show that the second argument is flawed as well. It is based on the identification of testing with robustness testing, where it is precisely the objective to find out how the system behaves under unspecified circumstances. This excludes the important activity of conformance testing, which tries to test the extent to which system behaviour conforms to its specification. It is precisely in this area where formal methods and tools can help to derive tests systematically from specifications, which is a great improvement over laborious, error-prone and costly manual test derivation. In our talk we show how the process algebraic testing theory due to De Nicola and Hennessy [DNH84,DeN87], originally conceived out of semantic considerations, may be used to obtain principles for test derivation. We will give an overview of the evolution of these ideas over the past ten years or so, starting with the conformance testing theory of simple synchronously communicating reactive systems [Bri88,Lan90] and leading to realistic systems that involve sophisticated asynchronous message passing mechanisms [Tre96,HT97]. Written accounts can be found in [BHT97,He98]. We discuss how such ideas have been used to obtain modern test derivation tools, such as TVEDA and TGV [Pha94, CGPT96,FJJV96], and the tool set that is currently being developed in the Côte-de-Resyste project [STW96]. The advantage of a test theory that is based on well-established process algebraic theory is that in principle there exists a clear link between testing and verification, which allows the areas to share ideas and algorithms [FJJV96,VT98]. Time allowing, we look at some of the methodological differences and commonalities between model checking techniques and testing, one of the differences being that of state space coverage, and an important commonality that of test property selection. In recent years the research into the use of formal methods and tools for testing reactive systems has seen a considerable growth. An overview of different approaches and school of thought can be found in [BPS98], reporting on the first ever Dagstuhl seminar devoted to testing. The formal treatment of conformance testing based on process algebra and/or concurrency theory is certainly not the only viable approach. An important school of thought is the FSM-testing theory grown out of the seminal work of Chow [Cho78], of which a good overview is given in [LY96]. Another interesting formal approach to testing is based on abstract data type theory [Gau95,BGM91].