Using Formal Specifications to Support Model Based Testing ASDSpec: A Tool Combining the Best of Two Techniques

A.P. van der Meer
R. Kherrazi
M. Hamilton

Formal methods and testing are two important approaches that assist in the development of high quality software. For long time these approaches have been seen as competitors and there was very little interaction between the two communities. In recent years a new consensus has developed in which they are seen as more complementary. In this report we present an approach based on the ASD(Analytical Software Design) suite by Verum and the Microsoft Spec Explorer Model Based Testing(MBT) tool. ASD is a model-based design approach that can produce verified software components that can be combined into complete systems. However, ASD cannot verify existing components, nor complex component interactions involving data transfers. We have developed a tool that allows us to convert ASD models to Spec Explorer, allowing us to do more complete verification of software systems using dynamic testing at little additional cost and effort. We demonstrate this by applying our approach to an industrial-size case study.

In Holger Schlingloff and Alexander K. Petrenko: Proceedings Ninth Workshop on Model-Based Testing (MBT 2014), Grenoble, France, 6 April 2014, Electronic Proceedings in Theoretical Computer Science 141, pp. 1–13.
Published: 27th March 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: