6 How Marrying Formal Methods and Testing Could Aid Component-based Systems

Using formal methods during the design process for building systems from components is prudent. Formal methods can prove properties about component wrappers. Formal methods can also foretell how well the components will interact with other components. Both of these applications of formal methods to component-based systems is beneficial and adds an engineering-like rigor to the process of software development.

But proofs are not foolproof. Informal methods such as testing and fault injection can decrease the likelihood that errors ``slip through the formal cracks'' by validating the claims made as a result of the formal analyses. For example, suppose that two components, A and B, are composed in the manner where A calls B. If we have proven certain properties about these two components in isolation, that information can be used to prove properties about A(B). Ideally, we would test the components in isolation as well as test the composite. Further, if a component is ``wrapped'' to nullify the possibility of certain outputs being produced, we can test to see if those outputs can be forced to occur via testing and/or fault injection testing.

Formal proofs are commonly used for showing that the composition between two ``good'' components will produce a ``good'' composite. (Here, ``good'' can refer to qualities as secure, correct, etc.) Ultimately, these proofs can be wrong, or the belief that the components are good could be in error. By testing the subsystem, confidence that the results from the proofs are correct is gained. This uses ``testing'' to test the accuracy of formal analyses while also testing the quality of the software.

Marrying these approaches would serve two specific purposes: one would be to determine when these approaches overlap in terms of the value-added to a program's quality, and the second would be to provide better data substantiating the claim that formal methods are cost-effective. Clearly, we cannot apply formal methods to all parts of today's enormous systems, and we need to apply formal methods to those regions where testing is least effective at detecting errors. There are certain classes of errors that each technique is likely to overlook, and it would be ideal to hone these techniques toward what they are good at and not chastise them for their deficiencies.

Component-based software development is slowly becoming a reality, and there are those that feel that formal methods, by themselves, will solve the key hurdles that are associated with building ``systems from systems.'' We take a more cautious stance and believe that the claims from using formal methods will always need to be tested out for each individual application.

The key impediment to component-based development becoming state-of-the-practice is the issue of component quality. If that problem were solved, and if a component consumer knew how an acquired component would behave in their environment after adoption, then the opportunity costs associated with selecting one component over the other could be better decided. Our research team at Reliable Software Technologies is currently working on one solution to this problem as discussed in the Background Section.

In summary, testing and formal methods are complementary approaches that can be leveraged to terrific advantage in component-based systems. We believe that a marriage between the two different approaches is long overdue.