Assertions are added to programs and can be checked at runtime; examples include preconditions, postconditions, monitor invariants, class invariants, check instructions and oracles. The inclusion of assertions with V&V can be advantageous by easing maintenance and testing and providing self-documenting code. The goal of this project is to determine whether or not integrating assertions with V&V technologies is cost-effective.
The first context that is being examined is that of multi-threaded programs (specifically in Java) which are hard to debug, test and verify. Synchronisation errors can easily be made that produce data race defects which can be hard to debug. Thus far, we have evaluated integrating Java PathFinder (JPF) [1] with assertions; JPF is a tool that integrates model checking, program analysis and testing. The study has been focusing on the common concurrent implementation BoundedBuffer. We are also looking into integrating assertions with noise makers (such as ConTest [2] and RaceFinder [3]) that insert calls to the yield() and sleep() functions into the code to increase the chance that running the program will reveal a defect.
The second context is the integration of assertions in model-based testing. Model-based testing is the automatic generation of efficient test procedures/vectors using models of system requirements. In this work, we are using a model-based testing tool, called NModel [4] for comparing simple conformance testing (CT) with and without (a) model-derived assertions (MDA), (b) MDAs augmented with implementation-guided assertions (IGA), and (c) assertions as oracles in the test drivers (ORC). The study examines various model-implementation pairs in C# and Java, mutating the implementations with defects, and then checking how the defects are detected using CT (a) without assertions, (b) with only MDAs and (c) with MDAs augmented with IGAs, (d) with only ORCs, (e) MDAs with ORCs, and (f) MDAs, IGAs with ORCs. So far we have investigated Magee and Kramer’s CruiseController program [5] and found that out of 15 bugs, 3 were found using MDAs with CT, 3 were found using MDAs and IGAs, 5 of the bugs were equivalent and 4 were not detected. In this simple case study, ORCs were included in MDAs. To build up our repository of components under test we are considering examples from the NModel suite [4].
In both contexts, the relevance of the results of the study greatly depends on the complexity and industrial applicability of the components under test.

References

[1] K. Havelund and T. Pressburger, "Model Checking Java Programs using Java PathFinder," International Journal of Software Tools for Technology Transfer (STTT), vol. 2, pp. 366-381, April 2000.
[2] O. Edelstein, E. Farchi, E. Goldin, Y. Nir, G. Ratsaby, and S. Ur, "Framework for testing multi-threaded Java programs," Concurrency and Computation: Practice and Experience, vol. 15, pp. 485-499, 2003.
[3] Y. Ben-Asher, Y. Eytani, and E. Farchi, "Heuristics for Finding Concurrent Bugs," in Workshop on Parallel and Distributed Testing and Debugging Nice, 2003.
[4] J. Jacky, M. Veanes, C. Campbell, and W. Schulte, Model-Based Software Testing and Analysis with C#: Cambridge University Press, 2008.
[5] J. Magee and J. Kramer, Concurrency: State Models & Java Programs: John Wiley & Sons, 1999.