Formal models and analysis for software component interaction testing

Abstract

An important problem in component-based software development is testing for correct interactions of components. A promising approach is to use formal state-space models and analysis techniques for effective and automated testing. however, existing techniques are not feasible as models and test cases are difficult enough for people to create, or alternatively, too complex for automatic tools to analyze.

To overcome these two problems, this thesis presents an object-oriented modelling language that is easy to use for software design, but it also has formal semantics to allows model to be re-used for interaction testing. Formal coverage criteria and test requirements can be defined for the models, and test cases can be generated using a model-checking approach. The thesis also presents new algorithms created to contain the state explosion that occurs in test generation from large models of software components. The algorithms allow the analysis of much larger models than previously possible. The feasibility of using these techniques for interaction testing is demonstrated by an experiment on the design of an example software system.